Users' Mathboxes 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 34806
Description: Technical lemma for bnj60 34824. 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 1909 . . . . . . . . . . . . . . . 16 𝑑 𝑅 FrSe 𝐴
8 bnj1445.5 . . . . . . . . . . . . . . . . . 18 𝐷 = {𝑥𝐴 ∣ ¬ ∃𝑓𝜏}
9 bnj1445.4 . . . . . . . . . . . . . . . . . . . . . 22 (𝜏 ↔ (𝑓𝐶 ∧ dom 𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅))))
10 bnj1445.3 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝐶 = {𝑓 ∣ ∃𝑑𝐵 (𝑓 Fn 𝑑 ∧ ∀𝑥𝑑 (𝑓𝑥) = (𝐺𝑌))}
11 nfre1 3272 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑑𝑑𝐵 (𝑓 Fn 𝑑 ∧ ∀𝑥𝑑 (𝑓𝑥) = (𝐺𝑌))
1211nfab 2897 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑑{𝑓 ∣ ∃𝑑𝐵 (𝑓 Fn 𝑑 ∧ ∀𝑥𝑑 (𝑓𝑥) = (𝐺𝑌))}
1310, 12nfcxfr 2889 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑑𝐶
1413nfcri 2882 . . . . . . . . . . . . . . . . . . . . . . 23 𝑑 𝑓𝐶
15 nfv 1909 . . . . . . . . . . . . . . . . . . . . . . 23 𝑑dom 𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅))
1614, 15nfan 1894 . . . . . . . . . . . . . . . . . . . . . 22 𝑑(𝑓𝐶 ∧ dom 𝑓 = ({𝑥} ∪ trCl(𝑥, 𝐴, 𝑅)))
179, 16nfxfr 1847 . . . . . . . . . . . . . . . . . . . . 21 𝑑𝜏
1817nfex 2312 . . . . . . . . . . . . . . . . . . . 20 𝑑𝑓𝜏
1918nfn 1852 . . . . . . . . . . . . . . . . . . 19 𝑑 ¬ ∃𝑓𝜏
20 nfcv 2891 . . . . . . . . . . . . . . . . . . 19 𝑑𝐴
2119, 20nfrabw 3456 . . . . . . . . . . . . . . . . . 18 𝑑{𝑥𝐴 ∣ ¬ ∃𝑓𝜏}
228, 21nfcxfr 2889 . . . . . . . . . . . . . . . . 17 𝑑𝐷
23 nfcv 2891 . . . . . . . . . . . . . . . . 17 𝑑
2422, 23nfne 3032 . . . . . . . . . . . . . . . 16 𝑑 𝐷 ≠ ∅
257, 24nfan 1894 . . . . . . . . . . . . . . 15 𝑑(𝑅 FrSe 𝐴𝐷 ≠ ∅)
266, 25nfxfr 1847 . . . . . . . . . . . . . 14 𝑑𝜓
2722nfcri 2882 . . . . . . . . . . . . . 14 𝑑 𝑥𝐷
28 nfv 1909 . . . . . . . . . . . . . . 15 𝑑 ¬ 𝑦𝑅𝑥
2922, 28nfralw 3298 . . . . . . . . . . . . . 14 𝑑𝑦𝐷 ¬ 𝑦𝑅𝑥
3026, 27, 29nf3an 1896 . . . . . . . . . . . . 13 𝑑(𝜓𝑥𝐷 ∧ ∀𝑦𝐷 ¬ 𝑦𝑅𝑥)
315, 30nfxfr 1847 . . . . . . . . . . . 12 𝑑𝜒
3231nf5ri 2183 . . . . . . . . . . 11 (𝜒 → ∀𝑑𝜒)
3332bnj1351 34588 . . . . . . . . . 10 ((𝜒𝑧𝐸) → ∀𝑑(𝜒𝑧𝐸))
3433nf5i 2134 . . . . . . . . 9 𝑑(𝜒𝑧𝐸)
354, 34nfxfr 1847 . . . . . . . 8 𝑑𝜃
36 nfv 1909 . . . . . . . 8 𝑑 𝑧 ∈ trCl(𝑥, 𝐴, 𝑅)
3735, 36nfan 1894 . . . . . . 7 𝑑(𝜃𝑧 ∈ trCl(𝑥, 𝐴, 𝑅))
383, 37nfxfr 1847 . . . . . 6 𝑑𝜁
39 bnj1445.9 . . . . . . . 8 𝐻 = {𝑓 ∣ ∃𝑦 ∈ pred (𝑥, 𝐴, 𝑅)𝜏′}
40 nfcv 2891 . . . . . . . . . 10 𝑑 pred(𝑥, 𝐴, 𝑅)
41 bnj1445.8 . . . . . . . . . . 11 (𝜏′[𝑦 / 𝑥]𝜏)
42 nfcv 2891 . . . . . . . . . . . 12 𝑑𝑦
4342, 17nfsbcw 3795 . . . . . . . . . . 11 𝑑[𝑦 / 𝑥]𝜏
4441, 43nfxfr 1847 . . . . . . . . . 10 𝑑𝜏′
4540, 44nfrexw 3300 . . . . . . . . 9 𝑑𝑦 ∈ pred (𝑥, 𝐴, 𝑅)𝜏′
4645nfab 2897 . . . . . . . 8 𝑑{𝑓 ∣ ∃𝑦 ∈ pred (𝑥, 𝐴, 𝑅)𝜏′}
4739, 46nfcxfr 2889 . . . . . . 7 𝑑𝐻
4847nfcri 2882 . . . . . 6 𝑑 𝑓𝐻
49 nfv 1909 . . . . . 6 𝑑 𝑧 ∈ dom 𝑓
5038, 48, 49nf3an 1896 . . . . 5 𝑑(𝜁𝑓𝐻𝑧 ∈ dom 𝑓)
512, 50nfxfr 1847 . . . 4 𝑑𝜌
5251nf5ri 2183 . . 3 (𝜌 → ∀𝑑𝜌)
53 ax-5 1905 . . 3 (𝑦 ∈ pred(𝑥, 𝐴, 𝑅) → ∀𝑑 𝑦 ∈ pred(𝑥, 𝐴, 𝑅))
5414nf5ri 2183 . . 3 (𝑓𝐶 → ∀𝑑 𝑓𝐶)
55 ax-5 1905 . . 3 (dom 𝑓 = ({𝑦} ∪ trCl(𝑦, 𝐴, 𝑅)) → ∀𝑑dom 𝑓 = ({𝑦} ∪ trCl(𝑦, 𝐴, 𝑅)))
5652, 53, 54, 55bnj982 34540 . 2 ((𝜌𝑦 ∈ pred(𝑥, 𝐴, 𝑅) ∧ 𝑓𝐶 ∧ dom 𝑓 = ({𝑦} ∪ trCl(𝑦, 𝐴, 𝑅))) → ∀𝑑(𝜌𝑦 ∈ pred(𝑥, 𝐴, 𝑅) ∧ 𝑓𝐶 ∧ dom 𝑓 = ({𝑦} ∪ trCl(𝑦, 𝐴, 𝑅))))
571, 56hbxfrbi 1819 1 (𝜎 → ∀𝑑𝜎)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 394  w3a 1084  wal 1531   = wceq 1533  wex 1773  wcel 2098  {cab 2702  wne 2929  wral 3050  wrex 3059  {crab 3418  [wsbc 3773  cun 3942  wss 3944  c0 4322  {csn 4630  cop 4636   cuni 4909   class class class wbr 5149  dom cdm 5678  cres 5680   Fn wfn 6544  cfv 6549  w-bnj17 34448   predc-bnj14 34450   FrSe w-bnj15 34454   trClc-bnj18 34456
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-ex 1774  df-nf 1778  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2930  df-ral 3051  df-rex 3060  df-rab 3419  df-sbc 3774  df-bnj17 34449
This theorem is referenced by:  bnj1450  34812
  Copyright terms: Public domain W3C validator