MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  zorn2lem4 Structured version   Visualization version   GIF version

Theorem zorn2lem4 10137
Description: Lemma for zorn2 10144. (Contributed by NM, 3-Apr-1997.) (Revised by Mario Carneiro, 9-May-2015.)
Hypotheses
Ref Expression
zorn2lem.3 𝐹 = recs((𝑓 ∈ V ↦ (𝑣𝐶𝑢𝐶 ¬ 𝑢𝑤𝑣)))
zorn2lem.4 𝐶 = {𝑧𝐴 ∣ ∀𝑔 ∈ ran 𝑓 𝑔𝑅𝑧}
zorn2lem.5 𝐷 = {𝑧𝐴 ∣ ∀𝑔 ∈ (𝐹𝑥)𝑔𝑅𝑧}
Assertion
Ref Expression
zorn2lem4 ((𝑅 Po 𝐴𝑤 We 𝐴) → ∃𝑥 ∈ On 𝐷 = ∅)
Distinct variable groups:   𝑓,𝑔,𝑢,𝑣,𝑤,𝑥,𝑧,𝐴   𝐷,𝑓,𝑢,𝑣   𝑓,𝐹,𝑔,𝑢,𝑣,𝑥,𝑧   𝑅,𝑓,𝑔,𝑢,𝑣,𝑤,𝑥,𝑧   𝑣,𝐶
Allowed substitution hints:   𝐶(𝑥,𝑧,𝑤,𝑢,𝑓,𝑔)   𝐷(𝑥,𝑧,𝑤,𝑔)   𝐹(𝑤)

Proof of Theorem zorn2lem4
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 pm3.24 406 . 2 ¬ (ran 𝐹 ∈ V ∧ ¬ ran 𝐹 ∈ V)
2 df-ne 2942 . . . . 5 (𝐷 ≠ ∅ ↔ ¬ 𝐷 = ∅)
32ralbii 3089 . . . 4 (∀𝑥 ∈ On 𝐷 ≠ ∅ ↔ ∀𝑥 ∈ On ¬ 𝐷 = ∅)
4 df-ral 3067 . . . 4 (∀𝑥 ∈ On 𝐷 ≠ ∅ ↔ ∀𝑥(𝑥 ∈ On → 𝐷 ≠ ∅))
5 ralnex 3162 . . . 4 (∀𝑥 ∈ On ¬ 𝐷 = ∅ ↔ ¬ ∃𝑥 ∈ On 𝐷 = ∅)
63, 4, 53bitr3i 304 . . 3 (∀𝑥(𝑥 ∈ On → 𝐷 ≠ ∅) ↔ ¬ ∃𝑥 ∈ On 𝐷 = ∅)
7 weso 5556 . . . . . . . . 9 (𝑤 We 𝐴𝑤 Or 𝐴)
87adantr 484 . . . . . . . 8 ((𝑤 We 𝐴 ∧ ∀𝑥(𝑥 ∈ On → 𝐷 ≠ ∅)) → 𝑤 Or 𝐴)
9 vex 3424 . . . . . . . 8 𝑤 ∈ V
10 soex 7717 . . . . . . . 8 ((𝑤 Or 𝐴𝑤 ∈ V) → 𝐴 ∈ V)
118, 9, 10sylancl 589 . . . . . . 7 ((𝑤 We 𝐴 ∧ ∀𝑥(𝑥 ∈ On → 𝐷 ≠ ∅)) → 𝐴 ∈ V)
12 zorn2lem.3 . . . . . . . . . . 11 𝐹 = recs((𝑓 ∈ V ↦ (𝑣𝐶𝑢𝐶 ¬ 𝑢𝑤𝑣)))
1312tfr1 8153 . . . . . . . . . 10 𝐹 Fn On
14 fvelrnb 6791 . . . . . . . . . 10 (𝐹 Fn On → (𝑦 ∈ ran 𝐹 ↔ ∃𝑥 ∈ On (𝐹𝑥) = 𝑦))
1513, 14ax-mp 5 . . . . . . . . 9 (𝑦 ∈ ran 𝐹 ↔ ∃𝑥 ∈ On (𝐹𝑥) = 𝑦)
16 nfv 1922 . . . . . . . . . . 11 𝑥 𝑤 We 𝐴
17 nfa1 2153 . . . . . . . . . . 11 𝑥𝑥(𝑥 ∈ On → 𝐷 ≠ ∅)
1816, 17nfan 1907 . . . . . . . . . 10 𝑥(𝑤 We 𝐴 ∧ ∀𝑥(𝑥 ∈ On → 𝐷 ≠ ∅))
19 nfv 1922 . . . . . . . . . 10 𝑥 𝑦𝐴
20 zorn2lem.5 . . . . . . . . . . . . . . . . . 18 𝐷 = {𝑧𝐴 ∣ ∀𝑔 ∈ (𝐹𝑥)𝑔𝑅𝑧}
2120ssrab3 4009 . . . . . . . . . . . . . . . . 17 𝐷𝐴
22 zorn2lem.4 . . . . . . . . . . . . . . . . . 18 𝐶 = {𝑧𝐴 ∣ ∀𝑔 ∈ ran 𝑓 𝑔𝑅𝑧}
2312, 22, 20zorn2lem1 10134 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ On ∧ (𝑤 We 𝐴𝐷 ≠ ∅)) → (𝐹𝑥) ∈ 𝐷)
2421, 23sselid 3912 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ On ∧ (𝑤 We 𝐴𝐷 ≠ ∅)) → (𝐹𝑥) ∈ 𝐴)
25 eleq1 2826 . . . . . . . . . . . . . . . 16 ((𝐹𝑥) = 𝑦 → ((𝐹𝑥) ∈ 𝐴𝑦𝐴))
2624, 25syl5ibcom 248 . . . . . . . . . . . . . . 15 ((𝑥 ∈ On ∧ (𝑤 We 𝐴𝐷 ≠ ∅)) → ((𝐹𝑥) = 𝑦𝑦𝐴))
2726exp32 424 . . . . . . . . . . . . . 14 (𝑥 ∈ On → (𝑤 We 𝐴 → (𝐷 ≠ ∅ → ((𝐹𝑥) = 𝑦𝑦𝐴))))
2827com12 32 . . . . . . . . . . . . 13 (𝑤 We 𝐴 → (𝑥 ∈ On → (𝐷 ≠ ∅ → ((𝐹𝑥) = 𝑦𝑦𝐴))))
2928a2d 29 . . . . . . . . . . . 12 (𝑤 We 𝐴 → ((𝑥 ∈ On → 𝐷 ≠ ∅) → (𝑥 ∈ On → ((𝐹𝑥) = 𝑦𝑦𝐴))))
3029spsd 2185 . . . . . . . . . . 11 (𝑤 We 𝐴 → (∀𝑥(𝑥 ∈ On → 𝐷 ≠ ∅) → (𝑥 ∈ On → ((𝐹𝑥) = 𝑦𝑦𝐴))))
3130imp 410 . . . . . . . . . 10 ((𝑤 We 𝐴 ∧ ∀𝑥(𝑥 ∈ On → 𝐷 ≠ ∅)) → (𝑥 ∈ On → ((𝐹𝑥) = 𝑦𝑦𝐴)))
3218, 19, 31rexlimd 3244 . . . . . . . . 9 ((𝑤 We 𝐴 ∧ ∀𝑥(𝑥 ∈ On → 𝐷 ≠ ∅)) → (∃𝑥 ∈ On (𝐹𝑥) = 𝑦𝑦𝐴))
3315, 32syl5bi 245 . . . . . . . 8 ((𝑤 We 𝐴 ∧ ∀𝑥(𝑥 ∈ On → 𝐷 ≠ ∅)) → (𝑦 ∈ ran 𝐹𝑦𝐴))
3433ssrdv 3921 . . . . . . 7 ((𝑤 We 𝐴 ∧ ∀𝑥(𝑥 ∈ On → 𝐷 ≠ ∅)) → ran 𝐹𝐴)
3511, 34ssexd 5231 . . . . . 6 ((𝑤 We 𝐴 ∧ ∀𝑥(𝑥 ∈ On → 𝐷 ≠ ∅)) → ran 𝐹 ∈ V)
3635ex 416 . . . . 5 (𝑤 We 𝐴 → (∀𝑥(𝑥 ∈ On → 𝐷 ≠ ∅) → ran 𝐹 ∈ V))
3736adantl 485 . . . 4 ((𝑅 Po 𝐴𝑤 We 𝐴) → (∀𝑥(𝑥 ∈ On → 𝐷 ≠ ∅) → ran 𝐹 ∈ V))
3812, 22, 20zorn2lem3 10136 . . . . . . . . . . . . . 14 ((𝑅 Po 𝐴 ∧ (𝑥 ∈ On ∧ (𝑤 We 𝐴𝐷 ≠ ∅))) → (𝑦𝑥 → ¬ (𝐹𝑥) = (𝐹𝑦)))
3938exp45 442 . . . . . . . . . . . . 13 (𝑅 Po 𝐴 → (𝑥 ∈ On → (𝑤 We 𝐴 → (𝐷 ≠ ∅ → (𝑦𝑥 → ¬ (𝐹𝑥) = (𝐹𝑦))))))
4039com23 86 . . . . . . . . . . . 12 (𝑅 Po 𝐴 → (𝑤 We 𝐴 → (𝑥 ∈ On → (𝐷 ≠ ∅ → (𝑦𝑥 → ¬ (𝐹𝑥) = (𝐹𝑦))))))
4140imp 410 . . . . . . . . . . 11 ((𝑅 Po 𝐴𝑤 We 𝐴) → (𝑥 ∈ On → (𝐷 ≠ ∅ → (𝑦𝑥 → ¬ (𝐹𝑥) = (𝐹𝑦)))))
4241a2d 29 . . . . . . . . . 10 ((𝑅 Po 𝐴𝑤 We 𝐴) → ((𝑥 ∈ On → 𝐷 ≠ ∅) → (𝑥 ∈ On → (𝑦𝑥 → ¬ (𝐹𝑥) = (𝐹𝑦)))))
4342imp4a 426 . . . . . . . . 9 ((𝑅 Po 𝐴𝑤 We 𝐴) → ((𝑥 ∈ On → 𝐷 ≠ ∅) → ((𝑥 ∈ On ∧ 𝑦𝑥) → ¬ (𝐹𝑥) = (𝐹𝑦))))
4443alrimdv 1937 . . . . . . . 8 ((𝑅 Po 𝐴𝑤 We 𝐴) → ((𝑥 ∈ On → 𝐷 ≠ ∅) → ∀𝑦((𝑥 ∈ On ∧ 𝑦𝑥) → ¬ (𝐹𝑥) = (𝐹𝑦))))
4544alimdv 1924 . . . . . . 7 ((𝑅 Po 𝐴𝑤 We 𝐴) → (∀𝑥(𝑥 ∈ On → 𝐷 ≠ ∅) → ∀𝑥𝑦((𝑥 ∈ On ∧ 𝑦𝑥) → ¬ (𝐹𝑥) = (𝐹𝑦))))
46 r2al 3123 . . . . . . 7 (∀𝑥 ∈ On ∀𝑦𝑥 ¬ (𝐹𝑥) = (𝐹𝑦) ↔ ∀𝑥𝑦((𝑥 ∈ On ∧ 𝑦𝑥) → ¬ (𝐹𝑥) = (𝐹𝑦)))
4745, 46syl6ibr 255 . . . . . 6 ((𝑅 Po 𝐴𝑤 We 𝐴) → (∀𝑥(𝑥 ∈ On → 𝐷 ≠ ∅) → ∀𝑥 ∈ On ∀𝑦𝑥 ¬ (𝐹𝑥) = (𝐹𝑦)))
48 ssid 3937 . . . . . . . 8 On ⊆ On
4913tz7.48lem 8197 . . . . . . . 8 ((On ⊆ On ∧ ∀𝑥 ∈ On ∀𝑦𝑥 ¬ (𝐹𝑥) = (𝐹𝑦)) → Fun (𝐹 ↾ On))
5048, 49mpan 690 . . . . . . 7 (∀𝑥 ∈ On ∀𝑦𝑥 ¬ (𝐹𝑥) = (𝐹𝑦) → Fun (𝐹 ↾ On))
51 fnrel 6498 . . . . . . . . . . 11 (𝐹 Fn On → Rel 𝐹)
5213, 51ax-mp 5 . . . . . . . . . 10 Rel 𝐹
5313fndmi 6500 . . . . . . . . . . 11 dom 𝐹 = On
5453eqimssi 3973 . . . . . . . . . 10 dom 𝐹 ⊆ On
55 relssres 5906 . . . . . . . . . 10 ((Rel 𝐹 ∧ dom 𝐹 ⊆ On) → (𝐹 ↾ On) = 𝐹)
5652, 54, 55mp2an 692 . . . . . . . . 9 (𝐹 ↾ On) = 𝐹
5756cnveqi 5757 . . . . . . . 8 (𝐹 ↾ On) = 𝐹
5857funeqi 6418 . . . . . . 7 (Fun (𝐹 ↾ On) ↔ Fun 𝐹)
5950, 58sylib 221 . . . . . 6 (∀𝑥 ∈ On ∀𝑦𝑥 ¬ (𝐹𝑥) = (𝐹𝑦) → Fun 𝐹)
6047, 59syl6 35 . . . . 5 ((𝑅 Po 𝐴𝑤 We 𝐴) → (∀𝑥(𝑥 ∈ On → 𝐷 ≠ ∅) → Fun 𝐹))
61 onprc 7580 . . . . . 6 ¬ On ∈ V
62 funrnex 7745 . . . . . . . 8 (dom 𝐹 ∈ V → (Fun 𝐹 → ran 𝐹 ∈ V))
6362com12 32 . . . . . . 7 (Fun 𝐹 → (dom 𝐹 ∈ V → ran 𝐹 ∈ V))
64 df-rn 5576 . . . . . . . 8 ran 𝐹 = dom 𝐹
6564eleq1i 2829 . . . . . . 7 (ran 𝐹 ∈ V ↔ dom 𝐹 ∈ V)
66 dfdm4 5778 . . . . . . . . 9 dom 𝐹 = ran 𝐹
6753, 66eqtr3i 2768 . . . . . . . 8 On = ran 𝐹
6867eleq1i 2829 . . . . . . 7 (On ∈ V ↔ ran 𝐹 ∈ V)
6963, 65, 683imtr4g 299 . . . . . 6 (Fun 𝐹 → (ran 𝐹 ∈ V → On ∈ V))
7061, 69mtoi 202 . . . . 5 (Fun 𝐹 → ¬ ran 𝐹 ∈ V)
7160, 70syl6 35 . . . 4 ((𝑅 Po 𝐴𝑤 We 𝐴) → (∀𝑥(𝑥 ∈ On → 𝐷 ≠ ∅) → ¬ ran 𝐹 ∈ V))
7237, 71jcad 516 . . 3 ((𝑅 Po 𝐴𝑤 We 𝐴) → (∀𝑥(𝑥 ∈ On → 𝐷 ≠ ∅) → (ran 𝐹 ∈ V ∧ ¬ ran 𝐹 ∈ V)))
736, 72syl5bir 246 . 2 ((𝑅 Po 𝐴𝑤 We 𝐴) → (¬ ∃𝑥 ∈ On 𝐷 = ∅ → (ran 𝐹 ∈ V ∧ ¬ ran 𝐹 ∈ V)))
741, 73mt3i 151 1 ((𝑅 Po 𝐴𝑤 We 𝐴) → ∃𝑥 ∈ On 𝐷 = ∅)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  wal 1541   = wceq 1543  wcel 2111  wne 2941  wral 3062  wrex 3063  {crab 3066  Vcvv 3420  wss 3880  c0 4251   class class class wbr 5067  cmpt 5149   Po wpo 5480   Or wor 5481   We wwe 5522  ccnv 5564  dom cdm 5565  ran crn 5566  cres 5567  cima 5568  Rel wrel 5570  Oncon0 6230  Fun wfun 6391   Fn wfn 6392  cfv 6397  crio 7187  recscrecs 8127
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2159  ax-12 2176  ax-ext 2709  ax-rep 5193  ax-sep 5206  ax-nul 5213  ax-pr 5336  ax-un 7541
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2072  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2887  df-ne 2942  df-ral 3067  df-rex 3068  df-reu 3069  df-rmo 3070  df-rab 3071  df-v 3422  df-sbc 3709  df-csb 3826  df-dif 3883  df-un 3885  df-in 3887  df-ss 3897  df-pss 3899  df-nul 4252  df-if 4454  df-sn 4556  df-pr 4558  df-tp 4560  df-op 4562  df-uni 4834  df-iun 4920  df-br 5068  df-opab 5130  df-mpt 5150  df-tr 5176  df-id 5469  df-eprel 5474  df-po 5482  df-so 5483  df-fr 5523  df-we 5525  df-xp 5571  df-rel 5572  df-cnv 5573  df-co 5574  df-dm 5575  df-rn 5576  df-res 5577  df-ima 5578  df-pred 6175  df-ord 6233  df-on 6234  df-suc 6236  df-iota 6355  df-fun 6399  df-fn 6400  df-f 6401  df-f1 6402  df-fo 6403  df-f1o 6404  df-fv 6405  df-riota 7188  df-wrecs 8067  df-recs 8128
This theorem is referenced by:  zorn2lem7  10140
  Copyright terms: Public domain W3C validator