Metamath Proof Explorer

Theorem zorn2lem7

Description: Lemma for zorn2 . (Contributed by NM, 6-Apr-1997) (Revised by Mario Carneiro, 9-May-2015)

Ref Expression
Hypotheses zorn2lem.3 ⊢F=recs⁡f∈V⟼ιv∈C|∀u∈C¬uwv
zorn2lem.4 ⊢C=z∈A|∀g∈ran⁡fgRz
zorn2lem.5 ⊢D=z∈A|∀g∈FxgRz
zorn2lem.7 ⊢H=z∈A|∀g∈FygRz
Assertion zorn2lem7 ⊢A∈dom⁡card∧RPoA∧∀ss⊆A∧ROrs→∃a∈A∀r∈srRa∨r=a→∃a∈A∀b∈A¬aRb

Proof

Step Hyp Ref Expression
1 zorn2lem.3 ⊢F=recs⁡f∈V⟼ιv∈C|∀u∈C¬uwv
2 zorn2lem.4 ⊢C=z∈A|∀g∈ran⁡fgRz
3 zorn2lem.5 ⊢D=z∈A|∀g∈FxgRz
4 zorn2lem.7 ⊢H=z∈A|∀g∈FygRz
5 ween ⊢A∈dom⁡card↔∃wwWeA
6 1 2 3 zorn2lem4 ⊢RPoA∧wWeA→∃x∈OnD=∅
7 imaeq2 ⊢x=y→Fx=Fy
8 7 raleqdv ⊢x=y→∀g∈FxgRz↔∀g∈FygRz
9 8 rabbidv ⊢x=y→z∈A|∀g∈FxgRz=z∈A|∀g∈FygRz
10 9 3 4 3eqtr4g ⊢x=y→D=H
11 10 eqeq1d ⊢x=y→D=∅↔H=∅
12 11 onminex ⊢∃x∈OnD=∅→∃x∈OnD=∅∧∀y∈x¬H=∅
13 df-ne ⊢H≠∅↔¬H=∅
14 13 ralbii ⊢∀y∈xH≠∅↔∀y∈x¬H=∅
15 14 anbi2i ⊢D=∅∧∀y∈xH≠∅↔D=∅∧∀y∈x¬H=∅
16 15 rexbii ⊢∃x∈OnD=∅∧∀y∈xH≠∅↔∃x∈OnD=∅∧∀y∈x¬H=∅
17 12 16 sylibr ⊢∃x∈OnD=∅→∃x∈OnD=∅∧∀y∈xH≠∅
18 1 2 3 4 zorn2lem5 ⊢wWeA∧x∈On∧∀y∈xH≠∅→Fx⊆A
19 18 a1i ⊢RPoA→wWeA∧x∈On∧∀y∈xH≠∅→Fx⊆A
20 1 2 3 4 zorn2lem6 ⊢RPoA→wWeA∧x∈On∧∀y∈xH≠∅→ROrFx
21 19 20 jcad ⊢RPoA→wWeA∧x∈On∧∀y∈xH≠∅→Fx⊆A∧ROrFx
22 1 tfr1 ⊢FFnOn
23 fnfun ⊢FFnOn→Fun⁡F
24 vex ⊢x∈V
25 24 funimaex ⊢Fun⁡F→Fx∈V
26 22 23 25 mp2b ⊢Fx∈V
27 sseq1 ⊢s=Fx→s⊆A↔Fx⊆A
28 soeq2 ⊢s=Fx→ROrs↔ROrFx
29 27 28 anbi12d ⊢s=Fx→s⊆A∧ROrs↔Fx⊆A∧ROrFx
30 raleq ⊢s=Fx→∀r∈srRa∨r=a↔∀r∈FxrRa∨r=a
31 30 rexbidv ⊢s=Fx→∃a∈A∀r∈srRa∨r=a↔∃a∈A∀r∈FxrRa∨r=a
32 29 31 imbi12d ⊢s=Fx→s⊆A∧ROrs→∃a∈A∀r∈srRa∨r=a↔Fx⊆A∧ROrFx→∃a∈A∀r∈FxrRa∨r=a
33 26 32 spcv ⊢∀ss⊆A∧ROrs→∃a∈A∀r∈srRa∨r=a→Fx⊆A∧ROrFx→∃a∈A∀r∈FxrRa∨r=a
34 21 33 sylan9 ⊢RPoA∧∀ss⊆A∧ROrs→∃a∈A∀r∈srRa∨r=a→wWeA∧x∈On∧∀y∈xH≠∅→∃a∈A∀r∈FxrRa∨r=a
35 34 adantld ⊢RPoA∧∀ss⊆A∧ROrs→∃a∈A∀r∈srRa∨r=a→D=∅∧wWeA∧x∈On∧∀y∈xH≠∅→∃a∈A∀r∈FxrRa∨r=a
36 35 imp ⊢RPoA∧∀ss⊆A∧ROrs→∃a∈A∀r∈srRa∨r=a∧D=∅∧wWeA∧x∈On∧∀y∈xH≠∅→∃a∈A∀r∈FxrRa∨r=a
37 noel ⊢¬b∈∅
38 18 sseld ⊢wWeA∧x∈On∧∀y∈xH≠∅→r∈Fx→r∈A
39 3anass ⊢r∈A∧a∈A∧b∈A↔r∈A∧a∈A∧b∈A
40 potr ⊢RPoA∧r∈A∧a∈A∧b∈A→rRa∧aRb→rRb
41 39 40 sylan2br ⊢RPoA∧r∈A∧a∈A∧b∈A→rRa∧aRb→rRb
42 41 expcomd ⊢RPoA∧r∈A∧a∈A∧b∈A→aRb→rRa→rRb
43 42 imp ⊢RPoA∧r∈A∧a∈A∧b∈A∧aRb→rRa→rRb
44 breq1 ⊢r=a→rRb↔aRb
45 44 biimprcd ⊢aRb→r=a→rRb
46 45 adantl ⊢RPoA∧r∈A∧a∈A∧b∈A∧aRb→r=a→rRb
47 43 46 jaod ⊢RPoA∧r∈A∧a∈A∧b∈A∧aRb→rRa∨r=a→rRb
48 47 exp42 ⊢RPoA→r∈A→a∈A∧b∈A→aRb→rRa∨r=a→rRb
49 38 48 sylan9r ⊢RPoA∧wWeA∧x∈On∧∀y∈xH≠∅→r∈Fx→a∈A∧b∈A→aRb→rRa∨r=a→rRb
50 49 com24 ⊢RPoA∧wWeA∧x∈On∧∀y∈xH≠∅→aRb→a∈A∧b∈A→r∈Fx→rRa∨r=a→rRb
51 50 com23 ⊢RPoA∧wWeA∧x∈On∧∀y∈xH≠∅→a∈A∧b∈A→aRb→r∈Fx→rRa∨r=a→rRb
52 51 imp31 ⊢RPoA∧wWeA∧x∈On∧∀y∈xH≠∅∧a∈A∧b∈A∧aRb→r∈Fx→rRa∨r=a→rRb
53 52 a2d ⊢RPoA∧wWeA∧x∈On∧∀y∈xH≠∅∧a∈A∧b∈A∧aRb→r∈Fx→rRa∨r=a→r∈Fx→rRb
54 53 ralimdv2 ⊢RPoA∧wWeA∧x∈On∧∀y∈xH≠∅∧a∈A∧b∈A∧aRb→∀r∈FxrRa∨r=a→∀r∈FxrRb
55 breq1 ⊢r=g→rRb↔gRb
56 55 cbvralvw ⊢∀r∈FxrRb↔∀g∈FxgRb
57 breq2 ⊢z=b→gRz↔gRb
58 57 ralbidv ⊢z=b→∀g∈FxgRz↔∀g∈FxgRb
59 58 elrab ⊢b∈z∈A|∀g∈FxgRz↔b∈A∧∀g∈FxgRb
60 3 eqeq1i ⊢D=∅↔z∈A|∀g∈FxgRz=∅
61 eleq2 ⊢z∈A|∀g∈FxgRz=∅→b∈z∈A|∀g∈FxgRz↔b∈∅
62 60 61 sylbi ⊢D=∅→b∈z∈A|∀g∈FxgRz↔b∈∅
63 59 62 bitr3id ⊢D=∅→b∈A∧∀g∈FxgRb↔b∈∅
64 63 biimpd ⊢D=∅→b∈A∧∀g∈FxgRb→b∈∅
65 64 expdimp ⊢D=∅∧b∈A→∀g∈FxgRb→b∈∅
66 56 65 biimtrid ⊢D=∅∧b∈A→∀r∈FxrRb→b∈∅
67 54 66 sylan9r ⊢D=∅∧b∈A∧RPoA∧wWeA∧x∈On∧∀y∈xH≠∅∧a∈A∧b∈A∧aRb→∀r∈FxrRa∨r=a→b∈∅
68 67 exp32 ⊢D=∅∧b∈A→RPoA∧wWeA∧x∈On∧∀y∈xH≠∅∧a∈A∧b∈A→aRb→∀r∈FxrRa∨r=a→b∈∅
69 68 com34 ⊢D=∅∧b∈A→RPoA∧wWeA∧x∈On∧∀y∈xH≠∅∧a∈A∧b∈A→∀r∈FxrRa∨r=a→aRb→b∈∅
70 69 imp31 ⊢D=∅∧b∈A∧RPoA∧wWeA∧x∈On∧∀y∈xH≠∅∧a∈A∧b∈A∧∀r∈FxrRa∨r=a→aRb→b∈∅
71 37 70 mtoi ⊢D=∅∧b∈A∧RPoA∧wWeA∧x∈On∧∀y∈xH≠∅∧a∈A∧b∈A∧∀r∈FxrRa∨r=a→¬aRb
72 71 exp42 ⊢D=∅∧b∈A→RPoA∧wWeA∧x∈On∧∀y∈xH≠∅→a∈A∧b∈A→∀r∈FxrRa∨r=a→¬aRb
73 72 exp4a ⊢D=∅∧b∈A→RPoA∧wWeA∧x∈On∧∀y∈xH≠∅→a∈A→b∈A→∀r∈FxrRa∨r=a→¬aRb
74 73 com34 ⊢D=∅∧b∈A→RPoA∧wWeA∧x∈On∧∀y∈xH≠∅→b∈A→a∈A→∀r∈FxrRa∨r=a→¬aRb
75 74 ex ⊢D=∅→b∈A→RPoA∧wWeA∧x∈On∧∀y∈xH≠∅→b∈A→a∈A→∀r∈FxrRa∨r=a→¬aRb
76 75 com4r ⊢b∈A→D=∅→b∈A→RPoA∧wWeA∧x∈On∧∀y∈xH≠∅→a∈A→∀r∈FxrRa∨r=a→¬aRb
77 76 pm2.43a ⊢b∈A→D=∅→RPoA∧wWeA∧x∈On∧∀y∈xH≠∅→a∈A→∀r∈FxrRa∨r=a→¬aRb
78 77 impd ⊢b∈A→D=∅∧RPoA∧wWeA∧x∈On∧∀y∈xH≠∅→a∈A→∀r∈FxrRa∨r=a→¬aRb
79 78 com4l ⊢D=∅∧RPoA∧wWeA∧x∈On∧∀y∈xH≠∅→a∈A→∀r∈FxrRa∨r=a→b∈A→¬aRb
80 79 impd ⊢D=∅∧RPoA∧wWeA∧x∈On∧∀y∈xH≠∅→a∈A∧∀r∈FxrRa∨r=a→b∈A→¬aRb
81 80 ralrimdv ⊢D=∅∧RPoA∧wWeA∧x∈On∧∀y∈xH≠∅→a∈A∧∀r∈FxrRa∨r=a→∀b∈A¬aRb
82 81 expd ⊢D=∅∧RPoA∧wWeA∧x∈On∧∀y∈xH≠∅→a∈A→∀r∈FxrRa∨r=a→∀b∈A¬aRb
83 82 reximdvai ⊢D=∅∧RPoA∧wWeA∧x∈On∧∀y∈xH≠∅→∃a∈A∀r∈FxrRa∨r=a→∃a∈A∀b∈A¬aRb
84 83 exp32 ⊢D=∅→RPoA→wWeA∧x∈On∧∀y∈xH≠∅→∃a∈A∀r∈FxrRa∨r=a→∃a∈A∀b∈A¬aRb
85 84 com12 ⊢RPoA→D=∅→wWeA∧x∈On∧∀y∈xH≠∅→∃a∈A∀r∈FxrRa∨r=a→∃a∈A∀b∈A¬aRb
86 85 adantr ⊢RPoA∧∀ss⊆A∧ROrs→∃a∈A∀r∈srRa∨r=a→D=∅→wWeA∧x∈On∧∀y∈xH≠∅→∃a∈A∀r∈FxrRa∨r=a→∃a∈A∀b∈A¬aRb
87 86 imp32 ⊢RPoA∧∀ss⊆A∧ROrs→∃a∈A∀r∈srRa∨r=a∧D=∅∧wWeA∧x∈On∧∀y∈xH≠∅→∃a∈A∀r∈FxrRa∨r=a→∃a∈A∀b∈A¬aRb
88 36 87 mpd ⊢RPoA∧∀ss⊆A∧ROrs→∃a∈A∀r∈srRa∨r=a∧D=∅∧wWeA∧x∈On∧∀y∈xH≠∅→∃a∈A∀b∈A¬aRb
89 88 exp45 ⊢RPoA∧∀ss⊆A∧ROrs→∃a∈A∀r∈srRa∨r=a→D=∅→wWeA∧x∈On→∀y∈xH≠∅→∃a∈A∀b∈A¬aRb
90 89 com23 ⊢RPoA∧∀ss⊆A∧ROrs→∃a∈A∀r∈srRa∨r=a→wWeA∧x∈On→D=∅→∀y∈xH≠∅→∃a∈A∀b∈A¬aRb
91 90 expdimp ⊢RPoA∧∀ss⊆A∧ROrs→∃a∈A∀r∈srRa∨r=a∧wWeA→x∈On→D=∅→∀y∈xH≠∅→∃a∈A∀b∈A¬aRb
92 91 imp4a ⊢RPoA∧∀ss⊆A∧ROrs→∃a∈A∀r∈srRa∨r=a∧wWeA→x∈On→D=∅∧∀y∈xH≠∅→∃a∈A∀b∈A¬aRb
93 92 com3l ⊢x∈On→D=∅∧∀y∈xH≠∅→RPoA∧∀ss⊆A∧ROrs→∃a∈A∀r∈srRa∨r=a∧wWeA→∃a∈A∀b∈A¬aRb
94 93 rexlimiv ⊢∃x∈OnD=∅∧∀y∈xH≠∅→RPoA∧∀ss⊆A∧ROrs→∃a∈A∀r∈srRa∨r=a∧wWeA→∃a∈A∀b∈A¬aRb
95 6 17 94 3syl ⊢RPoA∧wWeA→RPoA∧∀ss⊆A∧ROrs→∃a∈A∀r∈srRa∨r=a∧wWeA→∃a∈A∀b∈A¬aRb
96 95 adantlr ⊢RPoA∧∀ss⊆A∧ROrs→∃a∈A∀r∈srRa∨r=a∧wWeA→RPoA∧∀ss⊆A∧ROrs→∃a∈A∀r∈srRa∨r=a∧wWeA→∃a∈A∀b∈A¬aRb
97 96 pm2.43i ⊢RPoA∧∀ss⊆A∧ROrs→∃a∈A∀r∈srRa∨r=a∧wWeA→∃a∈A∀b∈A¬aRb
98 97 expcom ⊢wWeA→RPoA∧∀ss⊆A∧ROrs→∃a∈A∀r∈srRa∨r=a→∃a∈A∀b∈A¬aRb
99 98 exlimiv ⊢∃wwWeA→RPoA∧∀ss⊆A∧ROrs→∃a∈A∀r∈srRa∨r=a→∃a∈A∀b∈A¬aRb
100 5 99 sylbi ⊢A∈dom⁡card→RPoA∧∀ss⊆A∧ROrs→∃a∈A∀r∈srRa∨r=a→∃a∈A∀b∈A¬aRb
101 100 3impib ⊢A∈dom⁡card∧RPoA∧∀ss⊆A∧ROrs→∃a∈A∀r∈srRa∨r=a→∃a∈A∀b∈A¬aRb