Metamath Proof Explorer


Theorem aomclem8

Description: Lemma for dfac11 . Perform variable substitutions. This is the most we can say without invoking regularity. (Contributed by Stefan O'Rear, 20-Jan-2015)

Ref Expression
Hypotheses aomclem8.a φ A On
aomclem8.y φ a 𝒫 R1 A a y a 𝒫 a Fin
Assertion aomclem8 φ b b We R1 A

Proof

Step Hyp Ref Expression
1 aomclem8.a φ A On
2 aomclem8.y φ a 𝒫 R1 A a y a 𝒫 a Fin
3 elequ2 h = b i h i b
4 elequ2 g = c i g i c
5 4 notbid g = c ¬ i g ¬ i c
6 3 5 bi2anan9r g = c h = b i h ¬ i g i b ¬ i c
7 elequ2 g = c j g j c
8 elequ2 h = b j h j b
9 7 8 bi2bian9 g = c h = b j g j h j c j b
10 9 imbi2d g = c h = b j e dom e i j g j h j e dom e i j c j b
11 10 ralbidv g = c h = b j R1 dom e j e dom e i j g j h j R1 dom e j e dom e i j c j b
12 6 11 anbi12d g = c h = b i h ¬ i g j R1 dom e j e dom e i j g j h i b ¬ i c j R1 dom e j e dom e i j c j b
13 12 rexbidv g = c h = b i R1 dom e i h ¬ i g j R1 dom e j e dom e i j g j h i R1 dom e i b ¬ i c j R1 dom e j e dom e i j c j b
14 elequ1 i = d i b d b
15 elequ1 i = d i c d c
16 15 notbid i = d ¬ i c ¬ d c
17 14 16 anbi12d i = d i b ¬ i c d b ¬ d c
18 breq2 i = d j e dom e i j e dom e d
19 18 imbi1d i = d j e dom e i j c j b j e dom e d j c j b
20 19 ralbidv i = d j R1 dom e j e dom e i j c j b j R1 dom e j e dom e d j c j b
21 breq1 j = f j e dom e d f e dom e d
22 elequ1 j = f j c f c
23 elequ1 j = f j b f b
24 22 23 bibi12d j = f j c j b f c f b
25 21 24 imbi12d j = f j e dom e d j c j b f e dom e d f c f b
26 25 cbvralvw j R1 dom e j e dom e d j c j b f R1 dom e f e dom e d f c f b
27 20 26 bitrdi i = d j R1 dom e j e dom e i j c j b f R1 dom e f e dom e d f c f b
28 17 27 anbi12d i = d i b ¬ i c j R1 dom e j e dom e i j c j b d b ¬ d c f R1 dom e f e dom e d f c f b
29 28 cbvrexvw i R1 dom e i b ¬ i c j R1 dom e j e dom e i j c j b d R1 dom e d b ¬ d c f R1 dom e f e dom e d f c f b
30 13 29 bitrdi g = c h = b i R1 dom e i h ¬ i g j R1 dom e j e dom e i j g j h d R1 dom e d b ¬ d c f R1 dom e f e dom e d f c f b
31 30 cbvopabv g h | i R1 dom e i h ¬ i g j R1 dom e j e dom e i j g j h = c b | d R1 dom e d b ¬ d c f R1 dom e f e dom e d f c f b
32 nfcv _ c sup y g R1 dom e g h | i R1 dom e i h ¬ i g j R1 dom e j e dom e i j g j h
33 nfcv _ g y c
34 nfcv _ g R1 dom e
35 nfopab1 _ g g h | i R1 dom e i h ¬ i g j R1 dom e j e dom e i j g j h
36 33 34 35 nfsup _ g sup y c R1 dom e g h | i R1 dom e i h ¬ i g j R1 dom e j e dom e i j g j h
37 fveq2 g = c y g = y c
38 37 supeq1d g = c sup y g R1 dom e g h | i R1 dom e i h ¬ i g j R1 dom e j e dom e i j g j h = sup y c R1 dom e g h | i R1 dom e i h ¬ i g j R1 dom e j e dom e i j g j h
39 32 36 38 cbvmpt g V sup y g R1 dom e g h | i R1 dom e i h ¬ i g j R1 dom e j e dom e i j g j h = c V sup y c R1 dom e g h | i R1 dom e i h ¬ i g j R1 dom e j e dom e i j g j h
40 nfcv _ c g V sup y g R1 dom e g h | i R1 dom e i h ¬ i g j R1 dom e j e dom e i j g j h R1 dom e ran g
41 nffvmpt1 _ g g V sup y g R1 dom e g h | i R1 dom e i h ¬ i g j R1 dom e j e dom e i j g j h R1 dom e ran c
42 rneq g = c ran g = ran c
43 42 difeq2d g = c R1 dom e ran g = R1 dom e ran c
44 43 fveq2d g = c g V sup y g R1 dom e g h | i R1 dom e i h ¬ i g j R1 dom e j e dom e i j g j h R1 dom e ran g = g V sup y g R1 dom e g h | i R1 dom e i h ¬ i g j R1 dom e j e dom e i j g j h R1 dom e ran c
45 40 41 44 cbvmpt g V g V sup y g R1 dom e g h | i R1 dom e i h ¬ i g j R1 dom e j e dom e i j g j h R1 dom e ran g = c V g V sup y g R1 dom e g h | i R1 dom e i h ¬ i g j R1 dom e j e dom e i j g j h R1 dom e ran c
46 recseq g V g V sup y g R1 dom e g h | i R1 dom e i h ¬ i g j R1 dom e j e dom e i j g j h R1 dom e ran g = c V g V sup y g R1 dom e g h | i R1 dom e i h ¬ i g j R1 dom e j e dom e i j g j h R1 dom e ran c recs g V g V sup y g R1 dom e g h | i R1 dom e i h ¬ i g j R1 dom e j e dom e i j g j h R1 dom e ran g = recs c V g V sup y g R1 dom e g h | i R1 dom e i h ¬ i g j R1 dom e j e dom e i j g j h R1 dom e ran c
47 45 46 ax-mp recs g V g V sup y g R1 dom e g h | i R1 dom e i h ¬ i g j R1 dom e j e dom e i j g j h R1 dom e ran g = recs c V g V sup y g R1 dom e g h | i R1 dom e i h ¬ i g j R1 dom e j e dom e i j g j h R1 dom e ran c
48 nfv c recs g V g V sup y g R1 dom e g h | i R1 dom e i h ¬ i g j R1 dom e j e dom e i j g j h R1 dom e ran g -1 g recs g V g V sup y g R1 dom e g h | i R1 dom e i h ¬ i g j R1 dom e j e dom e i j g j h R1 dom e ran g -1 h
49 nfv b recs g V g V sup y g R1 dom e g h | i R1 dom e i h ¬ i g j R1 dom e j e dom e i j g j h R1 dom e ran g -1 g recs g V g V sup y g R1 dom e g h | i R1 dom e i h ¬ i g j R1 dom e j e dom e i j g j h R1 dom e ran g -1 h
50 nfmpt1 _ g g V g V sup y g R1 dom e g h | i R1 dom e i h ¬ i g j R1 dom e j e dom e i j g j h R1 dom e ran g
51 50 nfrecs _ g recs g V g V sup y g R1 dom e g h | i R1 dom e i h ¬ i g j R1 dom e j e dom e i j g j h R1 dom e ran g
52 51 nfcnv _ g recs g V g V sup y g R1 dom e g h | i R1 dom e i h ¬ i g j R1 dom e j e dom e i j g j h R1 dom e ran g -1
53 nfcv _ g c
54 52 53 nfima _ g recs g V g V sup y g R1 dom e g h | i R1 dom e i h ¬ i g j R1 dom e j e dom e i j g j h R1 dom e ran g -1 c
55 54 nfint _ g recs g V g V sup y g R1 dom e g h | i R1 dom e i h ¬ i g j R1 dom e j e dom e i j g j h R1 dom e ran g -1 c
56 nfcv _ g b
57 52 56 nfima _ g recs g V g V sup y g R1 dom e g h | i R1 dom e i h ¬ i g j R1 dom e j e dom e i j g j h R1 dom e ran g -1 b
58 57 nfint _ g recs g V g V sup y g R1 dom e g h | i R1 dom e i h ¬ i g j R1 dom e j e dom e i j g j h R1 dom e ran g -1 b
59 55 58 nfel g recs g V g V sup y g R1 dom e g h | i R1 dom e i h ¬ i g j R1 dom e j e dom e i j g j h R1 dom e ran g -1 c recs g V g V sup y g R1 dom e g h | i R1 dom e i h ¬ i g j R1 dom e j e dom e i j g j h R1 dom e ran g -1 b
60 nfcv _ h V
61 nfcv _ h y g
62 nfcv _ h R1 dom e
63 nfopab2 _ h g h | i R1 dom e i h ¬ i g j R1 dom e j e dom e i j g j h
64 61 62 63 nfsup _ h sup y g R1 dom e g h | i R1 dom e i h ¬ i g j R1 dom e j e dom e i j g j h
65 60 64 nfmpt _ h g V sup y g R1 dom e g h | i R1 dom e i h ¬ i g j R1 dom e j e dom e i j g j h
66 nfcv _ h R1 dom e ran g
67 65 66 nffv _ h g V sup y g R1 dom e g h | i R1 dom e i h ¬ i g j R1 dom e j e dom e i j g j h R1 dom e ran g
68 60 67 nfmpt _ h g V g V sup y g R1 dom e g h | i R1 dom e i h ¬ i g j R1 dom e j e dom e i j g j h R1 dom e ran g
69 68 nfrecs _ h recs g V g V sup y g R1 dom e g h | i R1 dom e i h ¬ i g j R1 dom e j e dom e i j g j h R1 dom e ran g
70 69 nfcnv _ h recs g V g V sup y g R1 dom e g h | i R1 dom e i h ¬ i g j R1 dom e j e dom e i j g j h R1 dom e ran g -1
71 nfcv _ h c
72 70 71 nfima _ h recs g V g V sup y g R1 dom e g h | i R1 dom e i h ¬ i g j R1 dom e j e dom e i j g j h R1 dom e ran g -1 c
73 72 nfint _ h recs g V g V sup y g R1 dom e g h | i R1 dom e i h ¬ i g j R1 dom e j e dom e i j g j h R1 dom e ran g -1 c
74 nfcv _ h b
75 70 74 nfima _ h recs g V g V sup y g R1 dom e g h | i R1 dom e i h ¬ i g j R1 dom e j e dom e i j g j h R1 dom e ran g -1 b
76 75 nfint _ h recs g V g V sup y g R1 dom e g h | i R1 dom e i h ¬ i g j R1 dom e j e dom e i j g j h R1 dom e ran g -1 b
77 73 76 nfel h recs g V g V sup y g R1 dom e g h | i R1 dom e i h ¬ i g j R1 dom e j e dom e i j g j h R1 dom e ran g -1 c recs g V g V sup y g R1 dom e g h | i R1 dom e i h ¬ i g j R1 dom e j e dom e i j g j h R1 dom e ran g -1 b
78 sneq g = c g = c
79 78 imaeq2d g = c recs g V g V sup y g R1 dom e g h | i R1 dom e i h ¬ i g j R1 dom e j e dom e i j g j h R1 dom e ran g -1 g = recs g V g V sup y g R1 dom e g h | i R1 dom e i h ¬ i g j R1 dom e j e dom e i j g j h R1 dom e ran g -1 c
80 79 inteqd g = c recs g V g V sup y g R1 dom e g h | i R1 dom e i h ¬ i g j R1 dom e j e dom e i j g j h R1 dom e ran g -1 g = recs g V g V sup y g R1 dom e g h | i R1 dom e i h ¬ i g j R1 dom e j e dom e i j g j h R1 dom e ran g -1 c
81 sneq h = b h = b
82 81 imaeq2d h = b recs g V g V sup y g R1 dom e g h | i R1 dom e i h ¬ i g j R1 dom e j e dom e i j g j h R1 dom e ran g -1 h = recs g V g V sup y g R1 dom e g h | i R1 dom e i h ¬ i g j R1 dom e j e dom e i j g j h R1 dom e ran g -1 b
83 82 inteqd h = b recs g V g V sup y g R1 dom e g h | i R1 dom e i h ¬ i g j R1 dom e j e dom e i j g j h R1 dom e ran g -1 h = recs g V g V sup y g R1 dom e g h | i R1 dom e i h ¬ i g j R1 dom e j e dom e i j g j h R1 dom e ran g -1 b
84 eleq12 recs g V g V sup y g R1 dom e g h | i R1 dom e i h ¬ i g j R1 dom e j e dom e i j g j h R1 dom e ran g -1 g = recs g V g V sup y g R1 dom e g h | i R1 dom e i h ¬ i g j R1 dom e j e dom e i j g j h R1 dom e ran g -1 c recs g V g V sup y g R1 dom e g h | i R1 dom e i h ¬ i g j R1 dom e j e dom e i j g j h R1 dom e ran g -1 h = recs g V g V sup y g R1 dom e g h | i R1 dom e i h ¬ i g j R1 dom e j e dom e i j g j h R1 dom e ran g -1 b recs g V g V sup y g R1 dom e g h | i R1 dom e i h ¬ i g j R1 dom e j e dom e i j g j h R1 dom e ran g -1 g recs g V g V sup y g R1 dom e g h | i R1 dom e i h ¬ i g j R1 dom e j e dom e i j g j h R1 dom e ran g -1 h recs g V g V sup y g R1 dom e g h | i R1 dom e i h ¬ i g j R1 dom e j e dom e i j g j h R1 dom e ran g -1 c recs g V g V sup y g R1 dom e g h | i R1 dom e i h ¬ i g j R1 dom e j e dom e i j g j h R1 dom e ran g -1 b
85 80 83 84 syl2an g = c h = b recs g V g V sup y g R1 dom e g h | i R1 dom e i h ¬ i g j R1 dom e j e dom e i j g j h R1 dom e ran g -1 g recs g V g V sup y g R1 dom e g h | i R1 dom e i h ¬ i g j R1 dom e j e dom e i j g j h R1 dom e ran g -1 h recs g V g V sup y g R1 dom e g h | i R1 dom e i h ¬ i g j R1 dom e j e dom e i j g j h R1 dom e ran g -1 c recs g V g V sup y g R1 dom e g h | i R1 dom e i h ¬ i g j R1 dom e j e dom e i j g j h R1 dom e ran g -1 b
86 48 49 59 77 85 cbvopab g h | recs g V g V sup y g R1 dom e g h | i R1 dom e i h ¬ i g j R1 dom e j e dom e i j g j h R1 dom e ran g -1 g recs g V g V sup y g R1 dom e g h | i R1 dom e i h ¬ i g j R1 dom e j e dom e i j g j h R1 dom e ran g -1 h = c b | recs g V g V sup y g R1 dom e g h | i R1 dom e i h ¬ i g j R1 dom e j e dom e i j g j h R1 dom e ran g -1 c recs g V g V sup y g R1 dom e g h | i R1 dom e i h ¬ i g j R1 dom e j e dom e i j g j h R1 dom e ran g -1 b
87 fveq2 g = c rank g = rank c
88 fveq2 h = b rank h = rank b
89 87 88 breqan12d g = c h = b rank g E rank h rank c E rank b
90 87 88 eqeqan12d g = c h = b rank g = rank h rank c = rank b
91 simpl g = c h = b g = c
92 suceq rank g = rank c suc rank g = suc rank c
93 87 92 syl g = c suc rank g = suc rank c
94 93 adantr g = c h = b suc rank g = suc rank c
95 94 fveq2d g = c h = b e suc rank g = e suc rank c
96 simpr g = c h = b h = b
97 91 95 96 breq123d g = c h = b g e suc rank g h c e suc rank c b
98 90 97 anbi12d g = c h = b rank g = rank h g e suc rank g h rank c = rank b c e suc rank c b
99 89 98 orbi12d g = c h = b rank g E rank h rank g = rank h g e suc rank g h rank c E rank b rank c = rank b c e suc rank c b
100 99 cbvopabv g h | rank g E rank h rank g = rank h g e suc rank g h = c b | rank c E rank b rank c = rank b c e suc rank c b
101 eqid if dom e = dom e g h | rank g E rank h rank g = rank h g e suc rank g h g h | recs g V g V sup y g R1 dom e g h | i R1 dom e i h ¬ i g j R1 dom e j e dom e i j g j h R1 dom e ran g -1 g recs g V g V sup y g R1 dom e g h | i R1 dom e i h ¬ i g j R1 dom e j e dom e i j g j h R1 dom e ran g -1 h R1 dom e × R1 dom e = if dom e = dom e g h | rank g E rank h rank g = rank h g e suc rank g h g h | recs g V g V sup y g R1 dom e g h | i R1 dom e i h ¬ i g j R1 dom e j e dom e i j g j h R1 dom e ran g -1 g recs g V g V sup y g R1 dom e g h | i R1 dom e i h ¬ i g j R1 dom e j e dom e i j g j h R1 dom e ran g -1 h R1 dom e × R1 dom e
102 dmeq l = e dom l = dom e
103 102 unieqd l = e dom l = dom e
104 102 103 eqeq12d l = e dom l = dom l dom e = dom e
105 fveq1 l = e l suc rank g = e suc rank g
106 105 breqd l = e g l suc rank g h g e suc rank g h
107 106 anbi2d l = e rank g = rank h g l suc rank g h rank g = rank h g e suc rank g h
108 107 orbi2d l = e rank g E rank h rank g = rank h g l suc rank g h rank g E rank h rank g = rank h g e suc rank g h
109 108 opabbidv l = e g h | rank g E rank h rank g = rank h g l suc rank g h = g h | rank g E rank h rank g = rank h g e suc rank g h
110 eqidd l = e y g = y g
111 102 fveq2d l = e R1 dom l = R1 dom e
112 103 fveq2d l = e R1 dom l = R1 dom e
113 id l = e l = e
114 113 103 fveq12d l = e l dom l = e dom e
115 114 breqd l = e j l dom l i j e dom e i
116 115 imbi1d l = e j l dom l i j g j h j e dom e i j g j h
117 112 116 raleqbidv l = e j R1 dom l j l dom l i j g j h j R1 dom e j e dom e i j g j h
118 117 anbi2d l = e i h ¬ i g j R1 dom l j l dom l i j g j h i h ¬ i g j R1 dom e j e dom e i j g j h
119 112 118 rexeqbidv l = e i R1 dom l i h ¬ i g j R1 dom l j l dom l i j g j h i R1 dom e i h ¬ i g j R1 dom e j e dom e i j g j h
120 119 opabbidv l = e g h | i R1 dom l i h ¬ i g j R1 dom l j l dom l i j g j h = g h | i R1 dom e i h ¬ i g j R1 dom e j e dom e i j g j h
121 110 111 120 supeq123d l = e sup y g R1 dom l g h | i R1 dom l i h ¬ i g j R1 dom l j l dom l i j g j h = sup y g R1 dom e g h | i R1 dom e i h ¬ i g j R1 dom e j e dom e i j g j h
122 121 mpteq2dv l = e g V sup y g R1 dom l g h | i R1 dom l i h ¬ i g j R1 dom l j l dom l i j g j h = g V sup y g R1 dom e g h | i R1 dom e i h ¬ i g j R1 dom e j e dom e i j g j h
123 111 difeq1d l = e R1 dom l ran g = R1 dom e ran g
124 122 123 fveq12d l = e g V sup y g R1 dom l g h | i R1 dom l i h ¬ i g j R1 dom l j l dom l i j g j h R1 dom l ran g = g V sup y g R1 dom e g h | i R1 dom e i h ¬ i g j R1 dom e j e dom e i j g j h R1 dom e ran g
125 124 mpteq2dv l = e g V g V sup y g R1 dom l g h | i R1 dom l i h ¬ i g j R1 dom l j l dom l i j g j h R1 dom l ran g = g V g V sup y g R1 dom e g h | i R1 dom e i h ¬ i g j R1 dom e j e dom e i j g j h R1 dom e ran g
126 recseq g V g V sup y g R1 dom l g h | i R1 dom l i h ¬ i g j R1 dom l j l dom l i j g j h R1 dom l ran g = g V g V sup y g R1 dom e g h | i R1 dom e i h ¬ i g j R1 dom e j e dom e i j g j h R1 dom e ran g recs g V g V sup y g R1 dom l g h | i R1 dom l i h ¬ i g j R1 dom l j l dom l i j g j h R1 dom l ran g = recs g V g V sup y g R1 dom e g h | i R1 dom e i h ¬ i g j R1 dom e j e dom e i j g j h R1 dom e ran g
127 125 126 syl l = e recs g V g V sup y g R1 dom l g h | i R1 dom l i h ¬ i g j R1 dom l j l dom l i j g j h R1 dom l ran g = recs g V g V sup y g R1 dom e g h | i R1 dom e i h ¬ i g j R1 dom e j e dom e i j g j h R1 dom e ran g
128 127 cnveqd l = e recs g V g V sup y g R1 dom l g h | i R1 dom l i h ¬ i g j R1 dom l j l dom l i j g j h R1 dom l ran g -1 = recs g V g V sup y g R1 dom e g h | i R1 dom e i h ¬ i g j R1 dom e j e dom e i j g j h R1 dom e ran g -1
129 128 imaeq1d l = e recs g V g V sup y g R1 dom l g h | i R1 dom l i h ¬ i g j R1 dom l j l dom l i j g j h R1 dom l ran g -1 g = recs g V g V sup y g R1 dom e g h | i R1 dom e i h ¬ i g j R1 dom e j e dom e i j g j h R1 dom e ran g -1 g
130 129 inteqd l = e recs g V g V sup y g R1 dom l g h | i R1 dom l i h ¬ i g j R1 dom l j l dom l i j g j h R1 dom l ran g -1 g = recs g V g V sup y g R1 dom e g h | i R1 dom e i h ¬ i g j R1 dom e j e dom e i j g j h R1 dom e ran g -1 g
131 128 imaeq1d l = e recs g V g V sup y g R1 dom l g h | i R1 dom l i h ¬ i g j R1 dom l j l dom l i j g j h R1 dom l ran g -1 h = recs g V g V sup y g R1 dom e g h | i R1 dom e i h ¬ i g j R1 dom e j e dom e i j g j h R1 dom e ran g -1 h
132 131 inteqd l = e recs g V g V sup y g R1 dom l g h | i R1 dom l i h ¬ i g j R1 dom l j l dom l i j g j h R1 dom l ran g -1 h = recs g V g V sup y g R1 dom e g h | i R1 dom e i h ¬ i g j R1 dom e j e dom e i j g j h R1 dom e ran g -1 h
133 130 132 eleq12d l = e recs g V g V sup y g R1 dom l g h | i R1 dom l i h ¬ i g j R1 dom l j l dom l i j g j h R1 dom l ran g -1 g recs g V g V sup y g R1 dom l g h | i R1 dom l i h ¬ i g j R1 dom l j l dom l i j g j h R1 dom l ran g -1 h recs g V g V sup y g R1 dom e g h | i R1 dom e i h ¬ i g j R1 dom e j e dom e i j g j h R1 dom e ran g -1 g recs g V g V sup y g R1 dom e g h | i R1 dom e i h ¬ i g j R1 dom e j e dom e i j g j h R1 dom e ran g -1 h
134 133 opabbidv l = e g h | recs g V g V sup y g R1 dom l g h | i R1 dom l i h ¬ i g j R1 dom l j l dom l i j g j h R1 dom l ran g -1 g recs g V g V sup y g R1 dom l g h | i R1 dom l i h ¬ i g j R1 dom l j l dom l i j g j h R1 dom l ran g -1 h = g h | recs g V g V sup y g R1 dom e g h | i R1 dom e i h ¬ i g j R1 dom e j e dom e i j g j h R1 dom e ran g -1 g recs g V g V sup y g R1 dom e g h | i R1 dom e i h ¬ i g j R1 dom e j e dom e i j g j h R1 dom e ran g -1 h
135 104 109 134 ifbieq12d l = e if dom l = dom l g h | rank g E rank h rank g = rank h g l suc rank g h g h | recs g V g V sup y g R1 dom l g h | i R1 dom l i h ¬ i g j R1 dom l j l dom l i j g j h R1 dom l ran g -1 g recs g V g V sup y g R1 dom l g h | i R1 dom l i h ¬ i g j R1 dom l j l dom l i j g j h R1 dom l ran g -1 h = if dom e = dom e g h | rank g E rank h rank g = rank h g e suc rank g h g h | recs g V g V sup y g R1 dom e g h | i R1 dom e i h ¬ i g j R1 dom e j e dom e i j g j h R1 dom e ran g -1 g recs g V g V sup y g R1 dom e g h | i R1 dom e i h ¬ i g j R1 dom e j e dom e i j g j h R1 dom e ran g -1 h
136 111 sqxpeqd l = e R1 dom l × R1 dom l = R1 dom e × R1 dom e
137 135 136 ineq12d l = e if dom l = dom l g h | rank g E rank h rank g = rank h g l suc rank g h g h | recs g V g V sup y g R1 dom l g h | i R1 dom l i h ¬ i g j R1 dom l j l dom l i j g j h R1 dom l ran g -1 g recs g V g V sup y g R1 dom l g h | i R1 dom l i h ¬ i g j R1 dom l j l dom l i j g j h R1 dom l ran g -1 h R1 dom l × R1 dom l = if dom e = dom e g h | rank g E rank h rank g = rank h g e suc rank g h g h | recs g V g V sup y g R1 dom e g h | i R1 dom e i h ¬ i g j R1 dom e j e dom e i j g j h R1 dom e ran g -1 g recs g V g V sup y g R1 dom e g h | i R1 dom e i h ¬ i g j R1 dom e j e dom e i j g j h R1 dom e ran g -1 h R1 dom e × R1 dom e
138 137 cbvmptv l V if dom l = dom l g h | rank g E rank h rank g = rank h g l suc rank g h g h | recs g V g V sup y g R1 dom l g h | i R1 dom l i h ¬ i g j R1 dom l j l dom l i j g j h R1 dom l ran g -1 g recs g V g V sup y g R1 dom l g h | i R1 dom l i h ¬ i g j R1 dom l j l dom l i j g j h R1 dom l ran g -1 h R1 dom l × R1 dom l = e V if dom e = dom e g h | rank g E rank h rank g = rank h g e suc rank g h g h | recs g V g V sup y g R1 dom e g h | i R1 dom e i h ¬ i g j R1 dom e j e dom e i j g j h R1 dom e ran g -1 g recs g V g V sup y g R1 dom e g h | i R1 dom e i h ¬ i g j R1 dom e j e dom e i j g j h R1 dom e ran g -1 h R1 dom e × R1 dom e
139 recseq l V if dom l = dom l g h | rank g E rank h rank g = rank h g l suc rank g h g h | recs g V g V sup y g R1 dom l g h | i R1 dom l i h ¬ i g j R1 dom l j l dom l i j g j h R1 dom l ran g -1 g recs g V g V sup y g R1 dom l g h | i R1 dom l i h ¬ i g j R1 dom l j l dom l i j g j h R1 dom l ran g -1 h R1 dom l × R1 dom l = e V if dom e = dom e g h | rank g E rank h rank g = rank h g e suc rank g h g h | recs g V g V sup y g R1 dom e g h | i R1 dom e i h ¬ i g j R1 dom e j e dom e i j g j h R1 dom e ran g -1 g recs g V g V sup y g R1 dom e g h | i R1 dom e i h ¬ i g j R1 dom e j e dom e i j g j h R1 dom e ran g -1 h R1 dom e × R1 dom e recs l V if dom l = dom l g h | rank g E rank h rank g = rank h g l suc rank g h g h | recs g V g V sup y g R1 dom l g h | i R1 dom l i h ¬ i g j R1 dom l j l dom l i j g j h R1 dom l ran g -1 g recs g V g V sup y g R1 dom l g h | i R1 dom l i h ¬ i g j R1 dom l j l dom l i j g j h R1 dom l ran g -1 h R1 dom l × R1 dom l = recs e V if dom e = dom e g h | rank g E rank h rank g = rank h g e suc rank g h g h | recs g V g V sup y g R1 dom e g h | i R1 dom e i h ¬ i g j R1 dom e j e dom e i j g j h R1 dom e ran g -1 g recs g V g V sup y g R1 dom e g h | i R1 dom e i h ¬ i g j R1 dom e j e dom e i j g j h R1 dom e ran g -1 h R1 dom e × R1 dom e
140 138 139 ax-mp recs l V if dom l = dom l g h | rank g E rank h rank g = rank h g l suc rank g h g h | recs g V g V sup y g R1 dom l g h | i R1 dom l i h ¬ i g j R1 dom l j l dom l i j g j h R1 dom l ran g -1 g recs g V g V sup y g R1 dom l g h | i R1 dom l i h ¬ i g j R1 dom l j l dom l i j g j h R1 dom l ran g -1 h R1 dom l × R1 dom l = recs e V if dom e = dom e g h | rank g E rank h rank g = rank h g e suc rank g h g h | recs g V g V sup y g R1 dom e g h | i R1 dom e i h ¬ i g j R1 dom e j e dom e i j g j h R1 dom e ran g -1 g recs g V g V sup y g R1 dom e g h | i R1 dom e i h ¬ i g j R1 dom e j e dom e i j g j h R1 dom e ran g -1 h R1 dom e × R1 dom e
141 neeq1 a = c a c
142 fveq2 a = c y a = y c
143 pweq a = c 𝒫 a = 𝒫 c
144 143 ineq1d a = c 𝒫 a Fin = 𝒫 c Fin
145 144 difeq1d a = c 𝒫 a Fin = 𝒫 c Fin
146 142 145 eleq12d a = c y a 𝒫 a Fin y c 𝒫 c Fin
147 141 146 imbi12d a = c a y a 𝒫 a Fin c y c 𝒫 c Fin
148 147 cbvralvw a 𝒫 R1 A a y a 𝒫 a Fin c 𝒫 R1 A c y c 𝒫 c Fin
149 2 148 sylib φ c 𝒫 R1 A c y c 𝒫 c Fin
150 31 39 47 86 100 101 140 1 149 aomclem7 φ b b We R1 A