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 ¬ 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
zorn2lem.7 H = z A | g F y g R z
Assertion zorn2lem7 A dom card R Po A s s A R Or s a A r s r R a r = a a A b A ¬ a R b

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 zorn2lem.7 H = z A | g F y g R z
5 ween A dom card w w We A
6 1 2 3 zorn2lem4 R Po A w We A x On D =
7 imaeq2 x = y F x = F y
8 7 raleqdv x = y g F x g R z g F y g R z
9 8 rabbidv x = y z A | g F x g R z = z A | g F y g R z
10 9 3 4 3eqtr4g x = y D = H
11 10 eqeq1d x = y D = H =
12 11 onminex x On D = x On D = y x ¬ H =
13 df-ne H ¬ H =
14 13 ralbii y x H y x ¬ H =
15 14 anbi2i D = y x H D = y x ¬ H =
16 15 rexbii x On D = y x H x On D = y x ¬ H =
17 12 16 sylibr x On D = x On D = y x H
18 1 2 3 4 zorn2lem5 w We A x On y x H F x A
19 18 a1i R Po A w We A x On y x H F x A
20 1 2 3 4 zorn2lem6 R Po A w We A x On y x H R Or F x
21 19 20 jcad R Po A w We A x On y x H F x A R Or F x
22 1 tfr1 F Fn On
23 fnfun F Fn On Fun F
24 vex x V
25 24 funimaex Fun F F x V
26 22 23 25 mp2b F x V
27 sseq1 s = F x s A F x A
28 soeq2 s = F x R Or s R Or F x
29 27 28 anbi12d s = F x s A R Or s F x A R Or F x
30 raleq s = F x r s r R a r = a r F x r R a r = a
31 30 rexbidv s = F x a A r s r R a r = a a A r F x r R a r = a
32 29 31 imbi12d s = F x s A R Or s a A r s r R a r = a F x A R Or F x a A r F x r R a r = a
33 26 32 spcv s s A R Or s a A r s r R a r = a F x A R Or F x a A r F x r R a r = a
34 21 33 sylan9 R Po A s s A R Or s a A r s r R a r = a w We A x On y x H a A r F x r R a r = a
35 34 adantld R Po A s s A R Or s a A r s r R a r = a D = w We A x On y x H a A r F x r R a r = a
36 35 imp R Po A s s A R Or s a A r s r R a r = a D = w We A x On y x H a A r F x r R a r = a
37 noel ¬ b
38 18 sseld w We A x On y x H r F x r A
39 3anass r A a A b A r A a A b A
40 potr R Po A r A a A b A r R a a R b r R b
41 39 40 sylan2br R Po A r A a A b A r R a a R b r R b
42 41 expcomd R Po A r A a A b A a R b r R a r R b
43 42 imp R Po A r A a A b A a R b r R a r R b
44 breq1 r = a r R b a R b
45 44 biimprcd a R b r = a r R b
46 45 adantl R Po A r A a A b A a R b r = a r R b
47 43 46 jaod R Po A r A a A b A a R b r R a r = a r R b
48 47 exp42 R Po A r A a A b A a R b r R a r = a r R b
49 38 48 sylan9r R Po A w We A x On y x H r F x a A b A a R b r R a r = a r R b
50 49 com24 R Po A w We A x On y x H a R b a A b A r F x r R a r = a r R b
51 50 com23 R Po A w We A x On y x H a A b A a R b r F x r R a r = a r R b
52 51 imp31 R Po A w We A x On y x H a A b A a R b r F x r R a r = a r R b
53 52 a2d R Po A w We A x On y x H a A b A a R b r F x r R a r = a r F x r R b
54 53 ralimdv2 R Po A w We A x On y x H a A b A a R b r F x r R a r = a r F x r R b
55 breq1 r = g r R b g R b
56 55 cbvralvw r F x r R b g F x g R b
57 breq2 z = b g R z g R b
58 57 ralbidv z = b g F x g R z g F x g R b
59 58 elrab b z A | g F x g R z b A g F x g R b
60 3 eqeq1i D = z A | g F x g R z =
61 eleq2 z A | g F x g R z = b z A | g F x g R z b
62 60 61 sylbi D = b z A | g F x g R z b
63 59 62 syl5bbr D = b A g F x g R b b
64 63 biimpd D = b A g F x g R b b
65 64 expdimp D = b A g F x g R b b
66 56 65 syl5bi D = b A r F x r R b b
67 54 66 sylan9r D = b A R Po A w We A x On y x H a A b A a R b r F x r R a r = a b
68 67 exp32 D = b A R Po A w We A x On y x H a A b A a R b r F x r R a r = a b
69 68 com34 D = b A R Po A w We A x On y x H a A b A r F x r R a r = a a R b b
70 69 imp31 D = b A R Po A w We A x On y x H a A b A r F x r R a r = a a R b b
71 37 70 mtoi D = b A R Po A w We A x On y x H a A b A r F x r R a r = a ¬ a R b
72 71 exp42 D = b A R Po A w We A x On y x H a A b A r F x r R a r = a ¬ a R b
73 72 exp4a D = b A R Po A w We A x On y x H a A b A r F x r R a r = a ¬ a R b
74 73 com34 D = b A R Po A w We A x On y x H b A a A r F x r R a r = a ¬ a R b
75 74 ex D = b A R Po A w We A x On y x H b A a A r F x r R a r = a ¬ a R b
76 75 com4r b A D = b A R Po A w We A x On y x H a A r F x r R a r = a ¬ a R b
77 76 pm2.43a b A D = R Po A w We A x On y x H a A r F x r R a r = a ¬ a R b
78 77 impd b A D = R Po A w We A x On y x H a A r F x r R a r = a ¬ a R b
79 78 com4l D = R Po A w We A x On y x H a A r F x r R a r = a b A ¬ a R b
80 79 impd D = R Po A w We A x On y x H a A r F x r R a r = a b A ¬ a R b
81 80 ralrimdv D = R Po A w We A x On y x H a A r F x r R a r = a b A ¬ a R b
82 81 expd D = R Po A w We A x On y x H a A r F x r R a r = a b A ¬ a R b
83 82 reximdvai D = R Po A w We A x On y x H a A r F x r R a r = a a A b A ¬ a R b
84 83 exp32 D = R Po A w We A x On y x H a A r F x r R a r = a a A b A ¬ a R b
85 84 com12 R Po A D = w We A x On y x H a A r F x r R a r = a a A b A ¬ a R b
86 85 adantr R Po A s s A R Or s a A r s r R a r = a D = w We A x On y x H a A r F x r R a r = a a A b A ¬ a R b
87 86 imp32 R Po A s s A R Or s a A r s r R a r = a D = w We A x On y x H a A r F x r R a r = a a A b A ¬ a R b
88 36 87 mpd R Po A s s A R Or s a A r s r R a r = a D = w We A x On y x H a A b A ¬ a R b
89 88 exp45 R Po A s s A R Or s a A r s r R a r = a D = w We A x On y x H a A b A ¬ a R b
90 89 com23 R Po A s s A R Or s a A r s r R a r = a w We A x On D = y x H a A b A ¬ a R b
91 90 expdimp R Po A s s A R Or s a A r s r R a r = a w We A x On D = y x H a A b A ¬ a R b
92 91 imp4a R Po A s s A R Or s a A r s r R a r = a w We A x On D = y x H a A b A ¬ a R b
93 92 com3l x On D = y x H R Po A s s A R Or s a A r s r R a r = a w We A a A b A ¬ a R b
94 93 rexlimiv x On D = y x H R Po A s s A R Or s a A r s r R a r = a w We A a A b A ¬ a R b
95 6 17 94 3syl R Po A w We A R Po A s s A R Or s a A r s r R a r = a w We A a A b A ¬ a R b
96 95 adantlr R Po A s s A R Or s a A r s r R a r = a w We A R Po A s s A R Or s a A r s r R a r = a w We A a A b A ¬ a R b
97 96 pm2.43i R Po A s s A R Or s a A r s r R a r = a w We A a A b A ¬ a R b
98 97 expcom w We A R Po A s s A R Or s a A r s r R a r = a a A b A ¬ a R b
99 98 exlimiv w w We A R Po A s s A R Or s a A r s r R a r = a a A b A ¬ a R b
100 5 99 sylbi A dom card R Po A s s A R Or s a A r s r R a r = a a A b A ¬ a R b
101 100 3impib A dom card R Po A s s A R Or s a A r s r R a r = a a A b A ¬ a R b