Mathbox for Jonathan Ben-Naim < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  bnj1445 Structured version   Visualization version   GIF version

Theorem bnj1445 31419
 Description: Technical lemma for bnj60 31437. This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
Hypotheses
Ref Expression
bnj1445.1 𝐵 = {𝑑 ∣ (𝑑𝐴 ∧ ∀𝑥𝑑 pred(𝑥, 𝐴, 𝑅) ⊆ 𝑑)}
bnj1445.2 𝑌 = ⟨𝑥, (𝑓 ↾ pred(𝑥, 𝐴, 𝑅))⟩
bnj1445.3 𝐶 = {𝑓 ∣ ∃𝑑𝐵 (𝑓 Fn 𝑑 ∧ ∀𝑥𝑑 (𝑓𝑥) = (𝐺𝑌))}
bnj1445.4 (𝜏 ↔ (𝑓𝐶 ∧ dom 𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅))))
bnj1445.5 𝐷 = {𝑥𝐴 ∣ ¬ ∃𝑓𝜏}
bnj1445.6 (𝜓 ↔ (𝑅 FrSe 𝐴𝐷 ≠ ∅))
bnj1445.7 (𝜒 ↔ (𝜓𝑥𝐷 ∧ ∀𝑦𝐷 ¬ 𝑦𝑅𝑥))
bnj1445.8 (𝜏′[𝑦 / 𝑥]𝜏)
bnj1445.9 𝐻 = {𝑓 ∣ ∃𝑦 ∈ pred (𝑥, 𝐴, 𝑅)𝜏′}
bnj1445.10 𝑃 = 𝐻
bnj1445.11 𝑍 = ⟨𝑥, (𝑃 ↾ pred(𝑥, 𝐴, 𝑅))⟩
bnj1445.12 𝑄 = (𝑃 ∪ {⟨𝑥, (𝐺𝑍)⟩})
bnj1445.13 𝑊 = ⟨𝑧, (𝑄 ↾ pred(𝑧, 𝐴, 𝑅))⟩
bnj1445.14 𝐸 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅))
bnj1445.15 (𝜒𝑃 Fn trCl(𝑥, 𝐴, 𝑅))
bnj1445.16 (𝜒𝑄 Fn ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅)))
bnj1445.17 (𝜃 ↔ (𝜒𝑧𝐸))
bnj1445.18 (𝜂 ↔ (𝜃𝑧 ∈ {𝑥}))
bnj1445.19 (𝜁 ↔ (𝜃𝑧 ∈ trCl(𝑥, 𝐴, 𝑅)))
bnj1445.20 (𝜌 ↔ (𝜁𝑓𝐻𝑧 ∈ dom 𝑓))
bnj1445.21 (𝜎 ↔ (𝜌𝑦 ∈ pred(𝑥, 𝐴, 𝑅) ∧ 𝑓𝐶 ∧ dom 𝑓 = ({𝑦} ∪ trCl(𝑦, 𝐴, 𝑅))))
bnj1445.22 (𝜑 ↔ (𝜎𝑑𝐵𝑓 Fn 𝑑 ∧ ∀𝑥𝑑 (𝑓𝑥) = (𝐺𝑌)))
bnj1445.23 𝑋 = ⟨𝑧, (𝑓 ↾ pred(𝑧, 𝐴, 𝑅))⟩
Assertion
Ref Expression
bnj1445 (𝜎 → ∀𝑑𝜎)
Distinct variable groups:   𝐴,𝑑,𝑥   𝐵,𝑓   𝐸,𝑑   𝑅,𝑑,𝑥   𝑓,𝑑,𝑥   𝑦,𝑑,𝑥   𝑧,𝑑
Allowed substitution hints:   𝜑(𝑥,𝑦,𝑧,𝑓,𝑑)   𝜓(𝑥,𝑦,𝑧,𝑓,𝑑)   𝜒(𝑥,𝑦,𝑧,𝑓,𝑑)   𝜃(𝑥,𝑦,𝑧,𝑓,𝑑)   𝜏(𝑥,𝑦,𝑧,𝑓,𝑑)   𝜂(𝑥,𝑦,𝑧,𝑓,𝑑)   𝜁(𝑥,𝑦,𝑧,𝑓,𝑑)   𝜎(𝑥,𝑦,𝑧,𝑓,𝑑)   𝜌(𝑥,𝑦,𝑧,𝑓,𝑑)   𝐴(𝑦,𝑧,𝑓)   𝐵(𝑥,𝑦,𝑧,𝑑)   𝐶(𝑥,𝑦,𝑧,𝑓,𝑑)   𝐷(𝑥,𝑦,𝑧,𝑓,𝑑)   𝑃(𝑥,𝑦,𝑧,𝑓,𝑑)   𝑄(𝑥,𝑦,𝑧,𝑓,𝑑)   𝑅(𝑦,𝑧,𝑓)   𝐸(𝑥,𝑦,𝑧,𝑓)   𝐺(𝑥,𝑦,𝑧,𝑓,𝑑)   𝐻(𝑥,𝑦,𝑧,𝑓,𝑑)   𝑊(𝑥,𝑦,𝑧,𝑓,𝑑)   𝑋(𝑥,𝑦,𝑧,𝑓,𝑑)   𝑌(𝑥,𝑦,𝑧,𝑓,𝑑)   𝑍(𝑥,𝑦,𝑧,𝑓,𝑑)   𝜏′(𝑥,𝑦,𝑧,𝑓,𝑑)

Proof of Theorem bnj1445
StepHypRef Expression
1 bnj1445.21 . 2 (𝜎 ↔ (𝜌𝑦 ∈ pred(𝑥, 𝐴, 𝑅) ∧ 𝑓𝐶 ∧ dom 𝑓 = ({𝑦} ∪ trCl(𝑦, 𝐴, 𝑅))))
2 bnj1445.20 . . . . 5 (𝜌 ↔ (𝜁𝑓𝐻𝑧 ∈ dom 𝑓))
3 bnj1445.19 . . . . . . 7 (𝜁 ↔ (𝜃𝑧 ∈ trCl(𝑥, 𝐴, 𝑅)))
4 bnj1445.17 . . . . . . . . 9 (𝜃 ↔ (𝜒𝑧𝐸))
5 bnj1445.7 . . . . . . . . . . . . 13 (𝜒 ↔ (𝜓𝑥𝐷 ∧ ∀𝑦𝐷 ¬ 𝑦𝑅𝑥))
6 bnj1445.6 . . . . . . . . . . . . . . 15 (𝜓 ↔ (𝑅 FrSe 𝐴𝐷 ≠ ∅))
7 nfv 1992 . . . . . . . . . . . . . . . 16 𝑑 𝑅 FrSe 𝐴
8 bnj1445.5 . . . . . . . . . . . . . . . . . 18 𝐷 = {𝑥𝐴 ∣ ¬ ∃𝑓𝜏}
9 bnj1445.4 . . . . . . . . . . . . . . . . . . . . . 22 (𝜏 ↔ (𝑓𝐶 ∧ dom 𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅))))
10 bnj1445.3 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝐶 = {𝑓 ∣ ∃𝑑𝐵 (𝑓 Fn 𝑑 ∧ ∀𝑥𝑑 (𝑓𝑥) = (𝐺𝑌))}
11 nfre1 3143 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑑𝑑𝐵 (𝑓 Fn 𝑑 ∧ ∀𝑥𝑑 (𝑓𝑥) = (𝐺𝑌))
1211nfab 2907 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑑{𝑓 ∣ ∃𝑑𝐵 (𝑓 Fn 𝑑 ∧ ∀𝑥𝑑 (𝑓𝑥) = (𝐺𝑌))}
1310, 12nfcxfr 2900 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑑𝐶
1413nfcri 2896 . . . . . . . . . . . . . . . . . . . . . . 23 𝑑 𝑓𝐶
15 nfv 1992 . . . . . . . . . . . . . . . . . . . . . . 23 𝑑dom 𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅))
1614, 15nfan 1977 . . . . . . . . . . . . . . . . . . . . . 22 𝑑(𝑓𝐶 ∧ dom 𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅)))
179, 16nfxfr 1928 . . . . . . . . . . . . . . . . . . . . 21 𝑑𝜏
1817nfex 2301 . . . . . . . . . . . . . . . . . . . 20 𝑑𝑓𝜏
1918nfn 1933 . . . . . . . . . . . . . . . . . . 19 𝑑 ¬ ∃𝑓𝜏
20 nfcv 2902 . . . . . . . . . . . . . . . . . . 19 𝑑𝐴
2119, 20nfrab 3262 . . . . . . . . . . . . . . . . . 18 𝑑{𝑥𝐴 ∣ ¬ ∃𝑓𝜏}
228, 21nfcxfr 2900 . . . . . . . . . . . . . . . . 17 𝑑𝐷
23 nfcv 2902 . . . . . . . . . . . . . . . . 17 𝑑
2422, 23nfne 3032 . . . . . . . . . . . . . . . 16 𝑑 𝐷 ≠ ∅
257, 24nfan 1977 . . . . . . . . . . . . . . 15 𝑑(𝑅 FrSe 𝐴𝐷 ≠ ∅)
266, 25nfxfr 1928 . . . . . . . . . . . . . 14 𝑑𝜓
2722nfcri 2896 . . . . . . . . . . . . . 14 𝑑 𝑥𝐷
28 nfv 1992 . . . . . . . . . . . . . . 15 𝑑 ¬ 𝑦𝑅𝑥
2922, 28nfral 3083 . . . . . . . . . . . . . 14 𝑑𝑦𝐷 ¬ 𝑦𝑅𝑥
3026, 27, 29nf3an 1980 . . . . . . . . . . . . 13 𝑑(𝜓𝑥𝐷 ∧ ∀𝑦𝐷 ¬ 𝑦𝑅𝑥)
315, 30nfxfr 1928 . . . . . . . . . . . 12 𝑑𝜒
3231nf5ri 2212 . . . . . . . . . . 11 (𝜒 → ∀𝑑𝜒)
3332bnj1351 31204 . . . . . . . . . 10 ((𝜒𝑧𝐸) → ∀𝑑(𝜒𝑧𝐸))
3433nf5i 2173 . . . . . . . . 9 𝑑(𝜒𝑧𝐸)
354, 34nfxfr 1928 . . . . . . . 8 𝑑𝜃
36 nfv 1992 . . . . . . . 8 𝑑 𝑧 ∈ trCl(𝑥, 𝐴, 𝑅)
3735, 36nfan 1977 . . . . . . 7 𝑑(𝜃𝑧 ∈ trCl(𝑥, 𝐴, 𝑅))
383, 37nfxfr 1928 . . . . . 6 𝑑𝜁
39 bnj1445.9 . . . . . . . 8 𝐻 = {𝑓 ∣ ∃𝑦 ∈ pred (𝑥, 𝐴, 𝑅)𝜏′}
40 nfcv 2902 . . . . . . . . . 10 𝑑 pred(𝑥, 𝐴, 𝑅)
41 bnj1445.8 . . . . . . . . . . 11 (𝜏′[𝑦 / 𝑥]𝜏)
42 nfcv 2902 . . . . . . . . . . . 12 𝑑𝑦
4342, 17nfsbc 3598 . . . . . . . . . . 11 𝑑[𝑦 / 𝑥]𝜏
4441, 43nfxfr 1928 . . . . . . . . . 10 𝑑𝜏′
4540, 44nfrex 3145 . . . . . . . . 9 𝑑𝑦 ∈ pred (𝑥, 𝐴, 𝑅)𝜏′
4645nfab 2907 . . . . . . . 8 𝑑{𝑓 ∣ ∃𝑦 ∈ pred (𝑥, 𝐴, 𝑅)𝜏′}
4739, 46nfcxfr 2900 . . . . . . 7 𝑑𝐻
4847nfcri 2896 . . . . . 6 𝑑 𝑓𝐻
49 nfv 1992 . . . . . 6 𝑑 𝑧 ∈ dom 𝑓
5038, 48, 49nf3an 1980 . . . . 5 𝑑(𝜁𝑓𝐻𝑧 ∈ dom 𝑓)
512, 50nfxfr 1928 . . . 4 𝑑𝜌
5251nf5ri 2212 . . 3 (𝜌 → ∀𝑑𝜌)
53 ax-5 1988 . . 3 (𝑦 ∈ pred(𝑥, 𝐴, 𝑅) → ∀𝑑 𝑦 ∈ pred(𝑥, 𝐴, 𝑅))
5414nf5ri 2212 . . 3 (𝑓𝐶 → ∀𝑑 𝑓𝐶)
55 ax-5 1988 . . 3 (dom 𝑓 = ({𝑦} ∪ trCl(𝑦, 𝐴, 𝑅)) → ∀𝑑dom 𝑓 = ({𝑦} ∪ trCl(𝑦, 𝐴, 𝑅)))
5652, 53, 54, 55bnj982 31156 . 2 ((𝜌𝑦 ∈ pred(𝑥, 𝐴, 𝑅) ∧ 𝑓𝐶 ∧ dom 𝑓 = ({𝑦} ∪ trCl(𝑦, 𝐴, 𝑅))) → ∀𝑑(𝜌𝑦 ∈ pred(𝑥, 𝐴, 𝑅) ∧ 𝑓𝐶 ∧ dom 𝑓 = ({𝑦} ∪ trCl(𝑦, 𝐴, 𝑅))))
571, 56hbxfrbi 1901 1 (𝜎 → ∀𝑑𝜎)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∧ wa 383   ∧ w3a 1072  ∀wal 1630   = wceq 1632  ∃wex 1853   ∈ wcel 2139  {cab 2746   ≠ wne 2932  ∀wral 3050  ∃wrex 3051  {crab 3054  [wsbc 3576   ∪ cun 3713   ⊆ wss 3715  ∅c0 4058  {csn 4321  ⟨cop 4327  ∪ cuni 4588   class class class wbr 4804  dom cdm 5266   ↾ cres 5268   Fn wfn 6044  ‘cfv 6049   ∧ w-bnj17 31061   predc-bnj14 31063   FrSe w-bnj15 31067   trClc-bnj18 31069 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-ral 3055  df-rex 3056  df-rab 3059  df-sbc 3577  df-bnj17 31062 This theorem is referenced by:  bnj1450  31425
 Copyright terms: Public domain W3C validator