Metamath Proof Explorer


Theorem zorn2lem4

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

Ref Expression
Hypotheses zorn2lem.3 F = recs f V ι v C | u C ¬ u w v
zorn2lem.4 C = z A | g ran f g R z
zorn2lem.5 D = z A | g F x g R z
Assertion zorn2lem4 R Po A w We A x On D =

Proof

Step Hyp Ref Expression
1 zorn2lem.3 F = recs f V ι v C | u C ¬ u w v
2 zorn2lem.4 C = z A | g ran f g R z
3 zorn2lem.5 D = z A | g F x g R z
4 pm3.24 ¬ ran F V ¬ ran F V
5 df-ne D ¬ D =
6 5 ralbii x On D x On ¬ D =
7 df-ral x On D x x On D
8 ralnex x On ¬ D = ¬ x On D =
9 6 7 8 3bitr3i x x On D ¬ x On D =
10 weso w We A w Or A
11 10 adantr w We A x x On D w Or A
12 vex w V
13 soex w Or A w V A V
14 11 12 13 sylancl w We A x x On D A V
15 1 tfr1 F Fn On
16 fvelrnb F Fn On y ran F x On F x = y
17 15 16 ax-mp y ran F x On F x = y
18 nfv x w We A
19 nfa1 x x x On D
20 18 19 nfan x w We A x x On D
21 nfv x y A
22 3 ssrab3 D A
23 1 2 3 zorn2lem1 x On w We A D F x D
24 22 23 sseldi x On w We A D F x A
25 eleq1 F x = y F x A y A
26 24 25 syl5ibcom x On w We A D F x = y y A
27 26 exp32 x On w We A D F x = y y A
28 27 com12 w We A x On D F x = y y A
29 28 a2d w We A x On D x On F x = y y A
30 29 spsd w We A x x On D x On F x = y y A
31 30 imp w We A x x On D x On F x = y y A
32 20 21 31 rexlimd w We A x x On D x On F x = y y A
33 17 32 syl5bi w We A x x On D y ran F y A
34 33 ssrdv w We A x x On D ran F A
35 14 34 ssexd w We A x x On D ran F V
36 35 ex w We A x x On D ran F V
37 36 adantl R Po A w We A x x On D ran F V
38 1 2 3 zorn2lem3 R Po A x On w We A D y x ¬ F x = F y
39 38 exp45 R Po A x On w We A D y x ¬ F x = F y
40 39 com23 R Po A w We A x On D y x ¬ F x = F y
41 40 imp R Po A w We A x On D y x ¬ F x = F y
42 41 a2d R Po A w We A x On D x On y x ¬ F x = F y
43 42 imp4a R Po A w We A x On D x On y x ¬ F x = F y
44 43 alrimdv R Po A w We A x On D y x On y x ¬ F x = F y
45 44 alimdv R Po A w We A x x On D x y x On y x ¬ F x = F y
46 r2al x On y x ¬ F x = F y x y x On y x ¬ F x = F y
47 45 46 syl6ibr R Po A w We A x x On D x On y x ¬ F x = F y
48 ssid On On
49 15 tz7.48lem On On x On y x ¬ F x = F y Fun F On -1
50 48 49 mpan x On y x ¬ F x = F y Fun F On -1
51 fnrel F Fn On Rel F
52 15 51 ax-mp Rel F
53 fndm F Fn On dom F = On
54 15 53 ax-mp dom F = On
55 54 eqimssi dom F On
56 relssres Rel F dom F On F On = F
57 52 55 56 mp2an F On = F
58 57 cnveqi F On -1 = F -1
59 58 funeqi Fun F On -1 Fun F -1
60 50 59 sylib x On y x ¬ F x = F y Fun F -1
61 47 60 syl6 R Po A w We A x x On D Fun F -1
62 onprc ¬ On V
63 funrnex dom F -1 V Fun F -1 ran F -1 V
64 63 com12 Fun F -1 dom F -1 V ran F -1 V
65 df-rn ran F = dom F -1
66 65 eleq1i ran F V dom F -1 V
67 dfdm4 dom F = ran F -1
68 54 67 eqtr3i On = ran F -1
69 68 eleq1i On V ran F -1 V
70 64 66 69 3imtr4g Fun F -1 ran F V On V
71 62 70 mtoi Fun F -1 ¬ ran F V
72 61 71 syl6 R Po A w We A x x On D ¬ ran F V
73 37 72 jcad R Po A w We A x x On D ran F V ¬ ran F V
74 9 73 syl5bir R Po A w We A ¬ x On D = ran F V ¬ ran F V
75 4 74 mt3i R Po A w We A x On D =