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

Theorem zorn2lem4 9913
Description: Lemma for zorn2 9920. (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 405 . 2 ¬ (ran 𝐹 ∈ V ∧ ¬ ran 𝐹 ∈ V)
2 df-ne 3015 . . . . 5 (𝐷 ≠ ∅ ↔ ¬ 𝐷 = ∅)
32ralbii 3163 . . . 4 (∀𝑥 ∈ On 𝐷 ≠ ∅ ↔ ∀𝑥 ∈ On ¬ 𝐷 = ∅)
4 df-ral 3141 . . . 4 (∀𝑥 ∈ On 𝐷 ≠ ∅ ↔ ∀𝑥(𝑥 ∈ On → 𝐷 ≠ ∅))
5 ralnex 3234 . . . 4 (∀𝑥 ∈ On ¬ 𝐷 = ∅ ↔ ¬ ∃𝑥 ∈ On 𝐷 = ∅)
63, 4, 53bitr3i 303 . . 3 (∀𝑥(𝑥 ∈ On → 𝐷 ≠ ∅) ↔ ¬ ∃𝑥 ∈ On 𝐷 = ∅)
7 weso 5539 . . . . . . . . 9 (𝑤 We 𝐴𝑤 Or 𝐴)
87adantr 483 . . . . . . . 8 ((𝑤 We 𝐴 ∧ ∀𝑥(𝑥 ∈ On → 𝐷 ≠ ∅)) → 𝑤 Or 𝐴)
9 vex 3496 . . . . . . . 8 𝑤 ∈ V
10 soex 7618 . . . . . . . 8 ((𝑤 Or 𝐴𝑤 ∈ V) → 𝐴 ∈ V)
118, 9, 10sylancl 588 . . . . . . 7 ((𝑤 We 𝐴 ∧ ∀𝑥(𝑥 ∈ On → 𝐷 ≠ ∅)) → 𝐴 ∈ V)
12 zorn2lem.3 . . . . . . . . . . 11 𝐹 = recs((𝑓 ∈ V ↦ (𝑣𝐶𝑢𝐶 ¬ 𝑢𝑤𝑣)))
1312tfr1 8025 . . . . . . . . . 10 𝐹 Fn On
14 fvelrnb 6719 . . . . . . . . . 10 (𝐹 Fn On → (𝑦 ∈ ran 𝐹 ↔ ∃𝑥 ∈ On (𝐹𝑥) = 𝑦))
1513, 14ax-mp 5 . . . . . . . . 9 (𝑦 ∈ ran 𝐹 ↔ ∃𝑥 ∈ On (𝐹𝑥) = 𝑦)
16 nfv 1909 . . . . . . . . . . 11 𝑥 𝑤 We 𝐴
17 nfa1 2149 . . . . . . . . . . 11 𝑥𝑥(𝑥 ∈ On → 𝐷 ≠ ∅)
1816, 17nfan 1894 . . . . . . . . . 10 𝑥(𝑤 We 𝐴 ∧ ∀𝑥(𝑥 ∈ On → 𝐷 ≠ ∅))
19 nfv 1909 . . . . . . . . . 10 𝑥 𝑦𝐴
20 zorn2lem.5 . . . . . . . . . . . . . . . . . 18 𝐷 = {𝑧𝐴 ∣ ∀𝑔 ∈ (𝐹𝑥)𝑔𝑅𝑧}
2120ssrab3 4055 . . . . . . . . . . . . . . . . 17 𝐷𝐴
22 zorn2lem.4 . . . . . . . . . . . . . . . . . 18 𝐶 = {𝑧𝐴 ∣ ∀𝑔 ∈ ran 𝑓 𝑔𝑅𝑧}
2312, 22, 20zorn2lem1 9910 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ On ∧ (𝑤 We 𝐴𝐷 ≠ ∅)) → (𝐹𝑥) ∈ 𝐷)
2421, 23sseldi 3963 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ On ∧ (𝑤 We 𝐴𝐷 ≠ ∅)) → (𝐹𝑥) ∈ 𝐴)
25 eleq1 2898 . . . . . . . . . . . . . . . 16 ((𝐹𝑥) = 𝑦 → ((𝐹𝑥) ∈ 𝐴𝑦𝐴))
2624, 25syl5ibcom 247 . . . . . . . . . . . . . . 15 ((𝑥 ∈ On ∧ (𝑤 We 𝐴𝐷 ≠ ∅)) → ((𝐹𝑥) = 𝑦𝑦𝐴))
2726exp32 423 . . . . . . . . . . . . . 14 (𝑥 ∈ On → (𝑤 We 𝐴 → (𝐷 ≠ ∅ → ((𝐹𝑥) = 𝑦𝑦𝐴))))
2827com12 32 . . . . . . . . . . . . 13 (𝑤 We 𝐴 → (𝑥 ∈ On → (𝐷 ≠ ∅ → ((𝐹𝑥) = 𝑦𝑦𝐴))))
2928a2d 29 . . . . . . . . . . . 12 (𝑤 We 𝐴 → ((𝑥 ∈ On → 𝐷 ≠ ∅) → (𝑥 ∈ On → ((𝐹𝑥) = 𝑦𝑦𝐴))))
3029spsd 2179 . . . . . . . . . . 11 (𝑤 We 𝐴 → (∀𝑥(𝑥 ∈ On → 𝐷 ≠ ∅) → (𝑥 ∈ On → ((𝐹𝑥) = 𝑦𝑦𝐴))))
3130imp 409 . . . . . . . . . 10 ((𝑤 We 𝐴 ∧ ∀𝑥(𝑥 ∈ On → 𝐷 ≠ ∅)) → (𝑥 ∈ On → ((𝐹𝑥) = 𝑦𝑦𝐴)))
3218, 19, 31rexlimd 3315 . . . . . . . . 9 ((𝑤 We 𝐴 ∧ ∀𝑥(𝑥 ∈ On → 𝐷 ≠ ∅)) → (∃𝑥 ∈ On (𝐹𝑥) = 𝑦𝑦𝐴))
3315, 32syl5bi 244 . . . . . . . 8 ((𝑤 We 𝐴 ∧ ∀𝑥(𝑥 ∈ On → 𝐷 ≠ ∅)) → (𝑦 ∈ ran 𝐹𝑦𝐴))
3433ssrdv 3971 . . . . . . 7 ((𝑤 We 𝐴 ∧ ∀𝑥(𝑥 ∈ On → 𝐷 ≠ ∅)) → ran 𝐹𝐴)
3511, 34ssexd 5219 . . . . . 6 ((𝑤 We 𝐴 ∧ ∀𝑥(𝑥 ∈ On → 𝐷 ≠ ∅)) → ran 𝐹 ∈ V)
3635ex 415 . . . . 5 (𝑤 We 𝐴 → (∀𝑥(𝑥 ∈ On → 𝐷 ≠ ∅) → ran 𝐹 ∈ V))
3736adantl 484 . . . 4 ((𝑅 Po 𝐴𝑤 We 𝐴) → (∀𝑥(𝑥 ∈ On → 𝐷 ≠ ∅) → ran 𝐹 ∈ V))
3812, 22, 20zorn2lem3 9912 . . . . . . . . . . . . . 14 ((𝑅 Po 𝐴 ∧ (𝑥 ∈ On ∧ (𝑤 We 𝐴𝐷 ≠ ∅))) → (𝑦𝑥 → ¬ (𝐹𝑥) = (𝐹𝑦)))
3938exp45 441 . . . . . . . . . . . . 13 (𝑅 Po 𝐴 → (𝑥 ∈ On → (𝑤 We 𝐴 → (𝐷 ≠ ∅ → (𝑦𝑥 → ¬ (𝐹𝑥) = (𝐹𝑦))))))
4039com23 86 . . . . . . . . . . . 12 (𝑅 Po 𝐴 → (𝑤 We 𝐴 → (𝑥 ∈ On → (𝐷 ≠ ∅ → (𝑦𝑥 → ¬ (𝐹𝑥) = (𝐹𝑦))))))
4140imp 409 . . . . . . . . . . 11 ((𝑅 Po 𝐴𝑤 We 𝐴) → (𝑥 ∈ On → (𝐷 ≠ ∅ → (𝑦𝑥 → ¬ (𝐹𝑥) = (𝐹𝑦)))))
4241a2d 29 . . . . . . . . . 10 ((𝑅 Po 𝐴𝑤 We 𝐴) → ((𝑥 ∈ On → 𝐷 ≠ ∅) → (𝑥 ∈ On → (𝑦𝑥 → ¬ (𝐹𝑥) = (𝐹𝑦)))))
4342imp4a 425 . . . . . . . . 9 ((𝑅 Po 𝐴𝑤 We 𝐴) → ((𝑥 ∈ On → 𝐷 ≠ ∅) → ((𝑥 ∈ On ∧ 𝑦𝑥) → ¬ (𝐹𝑥) = (𝐹𝑦))))
4443alrimdv 1924 . . . . . . . 8 ((𝑅 Po 𝐴𝑤 We 𝐴) → ((𝑥 ∈ On → 𝐷 ≠ ∅) → ∀𝑦((𝑥 ∈ On ∧ 𝑦𝑥) → ¬ (𝐹𝑥) = (𝐹𝑦))))
4544alimdv 1911 . . . . . . 7 ((𝑅 Po 𝐴𝑤 We 𝐴) → (∀𝑥(𝑥 ∈ On → 𝐷 ≠ ∅) → ∀𝑥𝑦((𝑥 ∈ On ∧ 𝑦𝑥) → ¬ (𝐹𝑥) = (𝐹𝑦))))
46 r2al 3199 . . . . . . 7 (∀𝑥 ∈ On ∀𝑦𝑥 ¬ (𝐹𝑥) = (𝐹𝑦) ↔ ∀𝑥𝑦((𝑥 ∈ On ∧ 𝑦𝑥) → ¬ (𝐹𝑥) = (𝐹𝑦)))
4745, 46syl6ibr 254 . . . . . 6 ((𝑅 Po 𝐴𝑤 We 𝐴) → (∀𝑥(𝑥 ∈ On → 𝐷 ≠ ∅) → ∀𝑥 ∈ On ∀𝑦𝑥 ¬ (𝐹𝑥) = (𝐹𝑦)))
48 ssid 3987 . . . . . . . 8 On ⊆ On
4913tz7.48lem 8069 . . . . . . . 8 ((On ⊆ On ∧ ∀𝑥 ∈ On ∀𝑦𝑥 ¬ (𝐹𝑥) = (𝐹𝑦)) → Fun (𝐹 ↾ On))
5048, 49mpan 688 . . . . . . 7 (∀𝑥 ∈ On ∀𝑦𝑥 ¬ (𝐹𝑥) = (𝐹𝑦) → Fun (𝐹 ↾ On))
51 fnrel 6447 . . . . . . . . . . 11 (𝐹 Fn On → Rel 𝐹)
5213, 51ax-mp 5 . . . . . . . . . 10 Rel 𝐹
53 fndm 6448 . . . . . . . . . . . 12 (𝐹 Fn On → dom 𝐹 = On)
5413, 53ax-mp 5 . . . . . . . . . . 11 dom 𝐹 = On
5554eqimssi 4023 . . . . . . . . . 10 dom 𝐹 ⊆ On
56 relssres 5886 . . . . . . . . . 10 ((Rel 𝐹 ∧ dom 𝐹 ⊆ On) → (𝐹 ↾ On) = 𝐹)
5752, 55, 56mp2an 690 . . . . . . . . 9 (𝐹 ↾ On) = 𝐹
5857cnveqi 5738 . . . . . . . 8 (𝐹 ↾ On) = 𝐹
5958funeqi 6369 . . . . . . 7 (Fun (𝐹 ↾ On) ↔ Fun 𝐹)
6050, 59sylib 220 . . . . . 6 (∀𝑥 ∈ On ∀𝑦𝑥 ¬ (𝐹𝑥) = (𝐹𝑦) → Fun 𝐹)
6147, 60syl6 35 . . . . 5 ((𝑅 Po 𝐴𝑤 We 𝐴) → (∀𝑥(𝑥 ∈ On → 𝐷 ≠ ∅) → Fun 𝐹))
62 onprc 7491 . . . . . 6 ¬ On ∈ V
63 funrnex 7647 . . . . . . . 8 (dom 𝐹 ∈ V → (Fun 𝐹 → ran 𝐹 ∈ V))
6463com12 32 . . . . . . 7 (Fun 𝐹 → (dom 𝐹 ∈ V → ran 𝐹 ∈ V))
65 df-rn 5559 . . . . . . . 8 ran 𝐹 = dom 𝐹
6665eleq1i 2901 . . . . . . 7 (ran 𝐹 ∈ V ↔ dom 𝐹 ∈ V)
67 dfdm4 5757 . . . . . . . . 9 dom 𝐹 = ran 𝐹
6854, 67eqtr3i 2844 . . . . . . . 8 On = ran 𝐹
6968eleq1i 2901 . . . . . . 7 (On ∈ V ↔ ran 𝐹 ∈ V)
7064, 66, 693imtr4g 298 . . . . . 6 (Fun 𝐹 → (ran 𝐹 ∈ V → On ∈ V))
7162, 70mtoi 201 . . . . 5 (Fun 𝐹 → ¬ ran 𝐹 ∈ V)
7261, 71syl6 35 . . . 4 ((𝑅 Po 𝐴𝑤 We 𝐴) → (∀𝑥(𝑥 ∈ On → 𝐷 ≠ ∅) → ¬ ran 𝐹 ∈ V))
7337, 72jcad 515 . . 3 ((𝑅 Po 𝐴𝑤 We 𝐴) → (∀𝑥(𝑥 ∈ On → 𝐷 ≠ ∅) → (ran 𝐹 ∈ V ∧ ¬ ran 𝐹 ∈ V)))
746, 73syl5bir 245 . 2 ((𝑅 Po 𝐴𝑤 We 𝐴) → (¬ ∃𝑥 ∈ On 𝐷 = ∅ → (ran 𝐹 ∈ V ∧ ¬ ran 𝐹 ∈ V)))
751, 74mt3i 151 1 ((𝑅 Po 𝐴𝑤 We 𝐴) → ∃𝑥 ∈ On 𝐷 = ∅)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 208  wa 398  wal 1529   = wceq 1531  wcel 2108  wne 3014  wral 3136  wrex 3137  {crab 3140  Vcvv 3493  wss 3934  c0 4289   class class class wbr 5057  cmpt 5137   Po wpo 5465   Or wor 5466   We wwe 5506  ccnv 5547  dom cdm 5548  ran crn 5549  cres 5550  cima 5551  Rel wrel 5553  Oncon0 6184  Fun wfun 6342   Fn wfn 6343  cfv 6348  crio 7105  recscrecs 7999
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2154  ax-12 2170  ax-ext 2791  ax-rep 5181  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7453
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1083  df-3an 1084  df-tru 1534  df-ex 1775  df-nf 1779  df-sb 2064  df-mo 2616  df-eu 2648  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ne 3015  df-ral 3141  df-rex 3142  df-reu 3143  df-rmo 3144  df-rab 3145  df-v 3495  df-sbc 3771  df-csb 3882  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-pss 3952  df-nul 4290  df-if 4466  df-sn 4560  df-pr 4562  df-tp 4564  df-op 4566  df-uni 4831  df-iun 4912  df-br 5058  df-opab 5120  df-mpt 5138  df-tr 5164  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-pred 6141  df-ord 6187  df-on 6188  df-suc 6190  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-riota 7106  df-wrecs 7939  df-recs 8000
This theorem is referenced by:  zorn2lem7  9916
  Copyright terms: Public domain W3C validator