Metamath Proof Explorer


Theorem aomclem6

Description: Lemma for dfac11 . Transfinite induction, close over z . (Contributed by Stefan O'Rear, 20-Jan-2015)

Ref Expression
Hypotheses aomclem6.b B = a b | c R1 dom z c b ¬ c a d R1 dom z d z dom z c d a d b
aomclem6.c C = a V sup y a R1 dom z B
aomclem6.d D = recs a V C R1 dom z ran a
aomclem6.e E = a b | D -1 a D -1 b
aomclem6.f F = a b | rank a E rank b rank a = rank b a z suc rank a b
aomclem6.g G = if dom z = dom z F E R1 dom z × R1 dom z
aomclem6.h H = recs z V G
aomclem6.a φ A On
aomclem6.y φ a 𝒫 R1 A a y a 𝒫 a Fin
Assertion aomclem6 φ H A We R1 A

Proof

Step Hyp Ref Expression
1 aomclem6.b B = a b | c R1 dom z c b ¬ c a d R1 dom z d z dom z c d a d b
2 aomclem6.c C = a V sup y a R1 dom z B
3 aomclem6.d D = recs a V C R1 dom z ran a
4 aomclem6.e E = a b | D -1 a D -1 b
5 aomclem6.f F = a b | rank a E rank b rank a = rank b a z suc rank a b
6 aomclem6.g G = if dom z = dom z F E R1 dom z × R1 dom z
7 aomclem6.h H = recs z V G
8 aomclem6.a φ A On
9 aomclem6.y φ a 𝒫 R1 A a y a 𝒫 a Fin
10 ssid A A
11 8 adantr φ A A A On
12 sseq1 c = d c A d A
13 12 anbi2d c = d φ c A φ d A
14 fveq2 c = d H c = H d
15 fveq2 c = d R1 c = R1 d
16 14 15 weeq12d c = d H c We R1 c H d We R1 d
17 13 16 imbi12d c = d φ c A H c We R1 c φ d A H d We R1 d
18 sseq1 c = A c A A A
19 18 anbi2d c = A φ c A φ A A
20 fveq2 c = A H c = H A
21 fveq2 c = A R1 c = R1 A
22 20 21 weeq12d c = A H c We R1 c H A We R1 A
23 19 22 imbi12d c = A φ c A H c We R1 c φ A A H A We R1 A
24 dmeq z = H c dom z = dom H c
25 24 adantl c On d c φ d A H d We R1 d φ c A z = H c dom z = dom H c
26 simpl1 c On d c φ d A H d We R1 d φ c A z = H c c On
27 onss c On c On
28 7 tfr1 H Fn On
29 fnssres H Fn On c On H c Fn c
30 28 29 mpan c On H c Fn c
31 fndm H c Fn c dom H c = c
32 26 27 30 31 4syl c On d c φ d A H d We R1 d φ c A z = H c dom H c = c
33 25 32 eqtrd c On d c φ d A H d We R1 d φ c A z = H c dom z = c
34 33 26 eqeltrd c On d c φ d A H d We R1 d φ c A z = H c dom z On
35 33 eleq2d c On d c φ d A H d We R1 d φ c A z = H c a dom z a c
36 35 biimpa c On d c φ d A H d We R1 d φ c A z = H c a dom z a c
37 simpll2 c On d c φ d A H d We R1 d φ c A z = H c a dom z d c φ d A H d We R1 d
38 simpl3l c On d c φ d A H d We R1 d φ c A z = H c φ
39 38 adantr c On d c φ d A H d We R1 d φ c A z = H c a dom z φ
40 onelss dom z On a dom z a dom z
41 34 40 syl c On d c φ d A H d We R1 d φ c A z = H c a dom z a dom z
42 41 imp c On d c φ d A H d We R1 d φ c A z = H c a dom z a dom z
43 simpl3r c On d c φ d A H d We R1 d φ c A z = H c c A
44 33 43 eqsstrd c On d c φ d A H d We R1 d φ c A z = H c dom z A
45 44 adantr c On d c φ d A H d We R1 d φ c A z = H c a dom z dom z A
46 42 45 sstrd c On d c φ d A H d We R1 d φ c A z = H c a dom z a A
47 sseq1 d = a d A a A
48 47 anbi2d d = a φ d A φ a A
49 fveq2 d = a H d = H a
50 fveq2 d = a R1 d = R1 a
51 49 50 weeq12d d = a H d We R1 d H a We R1 a
52 48 51 imbi12d d = a φ d A H d We R1 d φ a A H a We R1 a
53 52 rspcva a c d c φ d A H d We R1 d φ a A H a We R1 a
54 53 imp a c d c φ d A H d We R1 d φ a A H a We R1 a
55 36 37 39 46 54 syl22anc c On d c φ d A H d We R1 d φ c A z = H c a dom z H a We R1 a
56 fveq1 z = H c z a = H c a
57 56 ad2antlr c On d c φ d A H d We R1 d φ c A z = H c a dom z z a = H c a
58 fvres a c H c a = H a
59 36 58 syl c On d c φ d A H d We R1 d φ c A z = H c a dom z H c a = H a
60 57 59 eqtrd c On d c φ d A H d We R1 d φ c A z = H c a dom z z a = H a
61 weeq1 z a = H a z a We R1 a H a We R1 a
62 60 61 syl c On d c φ d A H d We R1 d φ c A z = H c a dom z z a We R1 a H a We R1 a
63 55 62 mpbird c On d c φ d A H d We R1 d φ c A z = H c a dom z z a We R1 a
64 63 ralrimiva c On d c φ d A H d We R1 d φ c A z = H c a dom z z a We R1 a
65 38 8 syl c On d c φ d A H d We R1 d φ c A z = H c A On
66 38 9 syl c On d c φ d A H d We R1 d φ c A z = H c a 𝒫 R1 A a y a 𝒫 a Fin
67 1 2 3 4 5 6 34 64 65 44 66 aomclem5 c On d c φ d A H d We R1 d φ c A z = H c G We R1 dom z
68 33 fveq2d c On d c φ d A H d We R1 d φ c A z = H c R1 dom z = R1 c
69 weeq2 R1 dom z = R1 c G We R1 dom z G We R1 c
70 68 69 syl c On d c φ d A H d We R1 d φ c A z = H c G We R1 dom z G We R1 c
71 67 70 mpbid c On d c φ d A H d We R1 d φ c A z = H c G We R1 c
72 71 ex c On d c φ d A H d We R1 d φ c A z = H c G We R1 c
73 72 alrimiv c On d c φ d A H d We R1 d φ c A z z = H c G We R1 c
74 nfv d z = H c G We R1 c
75 nfv z d = H c
76 nfsbc1v z [˙d / z]˙ G We R1 c
77 75 76 nfim z d = H c [˙d / z]˙ G We R1 c
78 eqeq1 z = d z = H c d = H c
79 sbceq1a z = d G We R1 c [˙d / z]˙ G We R1 c
80 78 79 imbi12d z = d z = H c G We R1 c d = H c [˙d / z]˙ G We R1 c
81 74 77 80 cbvalv1 z z = H c G We R1 c d d = H c [˙d / z]˙ G We R1 c
82 73 81 sylib c On d c φ d A H d We R1 d φ c A d d = H c [˙d / z]˙ G We R1 c
83 nfsbc1v d [˙ H c / d]˙ [˙d / z]˙ G We R1 c
84 fnfun H Fn On Fun H
85 28 84 ax-mp Fun H
86 vex c V
87 resfunexg Fun H c V H c V
88 85 86 87 mp2an H c V
89 sbceq1a d = H c [˙d / z]˙ G We R1 c [˙ H c / d]˙ [˙d / z]˙ G We R1 c
90 83 88 89 ceqsal d d = H c [˙d / z]˙ G We R1 c [˙ H c / d]˙ [˙d / z]˙ G We R1 c
91 82 90 sylib c On d c φ d A H d We R1 d φ c A [˙ H c / d]˙ [˙d / z]˙ G We R1 c
92 sbccow [˙ H c / d]˙ [˙d / z]˙ G We R1 c [˙ H c / z]˙ G We R1 c
93 91 92 sylib c On d c φ d A H d We R1 d φ c A [˙ H c / z]˙ G We R1 c
94 nfcsb1v _ z H c / z G
95 nfcv _ z R1 c
96 94 95 nfwe z H c / z G We R1 c
97 csbeq1a z = H c G = H c / z G
98 weeq1 G = H c / z G G We R1 c H c / z G We R1 c
99 97 98 syl z = H c G We R1 c H c / z G We R1 c
100 96 99 sbciegf H c V [˙ H c / z]˙ G We R1 c H c / z G We R1 c
101 88 100 ax-mp [˙ H c / z]˙ G We R1 c H c / z G We R1 c
102 93 101 sylib c On d c φ d A H d We R1 d φ c A H c / z G We R1 c
103 recsval c On recs z V G c = z V G recs z V G c
104 7 fveq1i H c = recs z V G c
105 fvex R1 dom z V
106 105 105 xpex R1 dom z × R1 dom z V
107 106 inex2 if dom z = dom z F E R1 dom z × R1 dom z V
108 6 107 eqeltri G V
109 108 csbex H c / z G V
110 eqid z V G = z V G
111 110 fvmpts H c V H c / z G V z V G H c = H c / z G
112 88 109 111 mp2an z V G H c = H c / z G
113 7 reseq1i H c = recs z V G c
114 113 fveq2i z V G H c = z V G recs z V G c
115 112 114 eqtr3i H c / z G = z V G recs z V G c
116 103 104 115 3eqtr4g c On H c = H c / z G
117 weeq1 H c = H c / z G H c We R1 c H c / z G We R1 c
118 116 117 syl c On H c We R1 c H c / z G We R1 c
119 118 3ad2ant1 c On d c φ d A H d We R1 d φ c A H c We R1 c H c / z G We R1 c
120 102 119 mpbird c On d c φ d A H d We R1 d φ c A H c We R1 c
121 120 3exp c On d c φ d A H d We R1 d φ c A H c We R1 c
122 17 23 121 tfis3 A On φ A A H A We R1 A
123 11 122 mpcom φ A A H A We R1 A
124 10 123 mpan2 φ H A We R1 A