Metamath Proof Explorer

Theorem hsmexlem4

Description: Lemma for hsmex . The core induction, establishing bounds on the order types of iterated unions of the initial set. (Contributed by Stefan O'Rear, 14-Feb-2015)

Ref Expression
Hypotheses hsmexlem4.x ⊢X∈V
hsmexlem4.h ⊢H=rec⁡z∈V⟼har⁡𝒫X×zhar⁡𝒫X↾ω
hsmexlem4.u ⊢U=x∈V⟼rec⁡y∈V⟼⋃yx↾ω
hsmexlem4.s ⊢S=a∈⋃R1On|∀b∈TC⁡ab≼X
hsmexlem4.o ⊢O=OrdIsoErankU⁡d⁡c
Assertion hsmexlem4 ⊢c∈ω∧d∈S→dom⁡O∈H⁡c

Proof

Step Hyp Ref Expression
1 hsmexlem4.x ⊢X∈V
2 hsmexlem4.h ⊢H=rec⁡z∈V⟼har⁡𝒫X×zhar⁡𝒫X↾ω
3 hsmexlem4.u ⊢U=x∈V⟼rec⁡y∈V⟼⋃yx↾ω
4 hsmexlem4.s ⊢S=a∈⋃R1On|∀b∈TC⁡ab≼X
5 hsmexlem4.o ⊢O=OrdIsoErankU⁡d⁡c
6 fveq2 ⊢c=∅→U⁡d⁡c=U⁡d⁡∅
7 6 imaeq2d ⊢c=∅→rankU⁡d⁡c=rankU⁡d⁡∅
8 oieq2 ⊢rankU⁡d⁡c=rankU⁡d⁡∅→OrdIsoErankU⁡d⁡c=OrdIsoErankU⁡d⁡∅
9 7 8 syl ⊢c=∅→OrdIsoErankU⁡d⁡c=OrdIsoErankU⁡d⁡∅
10 5 9 eqtrid ⊢c=∅→O=OrdIsoErankU⁡d⁡∅
11 10 dmeqd ⊢c=∅→dom⁡O=dom⁡OrdIsoErankU⁡d⁡∅
12 fveq2 ⊢c=∅→H⁡c=H⁡∅
13 11 12 eleq12d ⊢c=∅→dom⁡O∈H⁡c↔dom⁡OrdIsoErankU⁡d⁡∅∈H⁡∅
14 13 ralbidv ⊢c=∅→∀d∈Sdom⁡O∈H⁡c↔∀d∈Sdom⁡OrdIsoErankU⁡d⁡∅∈H⁡∅
15 fveq2 ⊢c=e→U⁡d⁡c=U⁡d⁡e
16 15 imaeq2d ⊢c=e→rankU⁡d⁡c=rankU⁡d⁡e
17 oieq2 ⊢rankU⁡d⁡c=rankU⁡d⁡e→OrdIsoErankU⁡d⁡c=OrdIsoErankU⁡d⁡e
18 16 17 syl ⊢c=e→OrdIsoErankU⁡d⁡c=OrdIsoErankU⁡d⁡e
19 5 18 eqtrid ⊢c=e→O=OrdIsoErankU⁡d⁡e
20 19 dmeqd ⊢c=e→dom⁡O=dom⁡OrdIsoErankU⁡d⁡e
21 fveq2 ⊢c=e→H⁡c=H⁡e
22 20 21 eleq12d ⊢c=e→dom⁡O∈H⁡c↔dom⁡OrdIsoErankU⁡d⁡e∈H⁡e
23 22 ralbidv ⊢c=e→∀d∈Sdom⁡O∈H⁡c↔∀d∈Sdom⁡OrdIsoErankU⁡d⁡e∈H⁡e
24 fveq2 ⊢c=suc⁡e→U⁡d⁡c=U⁡d⁡suc⁡e
25 24 imaeq2d ⊢c=suc⁡e→rankU⁡d⁡c=rankU⁡d⁡suc⁡e
26 oieq2 ⊢rankU⁡d⁡c=rankU⁡d⁡suc⁡e→OrdIsoErankU⁡d⁡c=OrdIsoErankU⁡d⁡suc⁡e
27 25 26 syl ⊢c=suc⁡e→OrdIsoErankU⁡d⁡c=OrdIsoErankU⁡d⁡suc⁡e
28 5 27 eqtrid ⊢c=suc⁡e→O=OrdIsoErankU⁡d⁡suc⁡e
29 28 dmeqd ⊢c=suc⁡e→dom⁡O=dom⁡OrdIsoErankU⁡d⁡suc⁡e
30 fveq2 ⊢c=suc⁡e→H⁡c=H⁡suc⁡e
31 29 30 eleq12d ⊢c=suc⁡e→dom⁡O∈H⁡c↔dom⁡OrdIsoErankU⁡d⁡suc⁡e∈H⁡suc⁡e
32 31 ralbidv ⊢c=suc⁡e→∀d∈Sdom⁡O∈H⁡c↔∀d∈Sdom⁡OrdIsoErankU⁡d⁡suc⁡e∈H⁡suc⁡e
33 imassrn ⊢rankU⁡d⁡∅⊆ran⁡rank
34 rankf ⊢rank:⋃R1On⟶On
35 frn ⊢rank:⋃R1On⟶On→ran⁡rank⊆On
36 34 35 ax-mp ⊢ran⁡rank⊆On
37 33 36 sstri ⊢rankU⁡d⁡∅⊆On
38 3 ituni0 ⊢d∈V→U⁡d⁡∅=d
39 38 elv ⊢U⁡d⁡∅=d
40 39 imaeq2i ⊢rankU⁡d⁡∅=rankd
41 ffun ⊢rank:⋃R1On⟶On→Fun⁡rank
42 34 41 ax-mp ⊢Fun⁡rank
43 vex ⊢d∈V
44 wdomimag ⊢Fun⁡rank∧d∈V→rankd≼*d
45 42 43 44 mp2an ⊢rankd≼*d
46 sneq ⊢a=d→a=d
47 46 fveq2d ⊢a=d→TC⁡a=TC⁡d
48 47 raleqdv ⊢a=d→∀b∈TC⁡ab≼X↔∀b∈TC⁡db≼X
49 48 4 elrab2 ⊢d∈S↔d∈⋃R1On∧∀b∈TC⁡db≼X
50 49 simprbi ⊢d∈S→∀b∈TC⁡db≼X
51 vsnex ⊢d∈V
52 tcid ⊢d∈V→d⊆TC⁡d
53 51 52 ax-mp ⊢d⊆TC⁡d
54 vsnid ⊢d∈d
55 53 54 sselii ⊢d∈TC⁡d
56 breq1 ⊢b=d→b≼X↔d≼X
57 56 rspcv ⊢d∈TC⁡d→∀b∈TC⁡db≼X→d≼X
58 55 57 ax-mp ⊢∀b∈TC⁡db≼X→d≼X
59 domwdom ⊢d≼X→d≼*X
60 50 58 59 3syl ⊢d∈S→d≼*X
61 wdomtr ⊢rankd≼*d∧d≼*X→rankd≼*X
62 45 60 61 sylancr ⊢d∈S→rankd≼*X
63 40 62 eqbrtrid ⊢d∈S→rankU⁡d⁡∅≼*X
64 eqid ⊢OrdIsoErankU⁡d⁡∅=OrdIsoErankU⁡d⁡∅
65 64 hsmexlem1 ⊢rankU⁡d⁡∅⊆On∧rankU⁡d⁡∅≼*X→dom⁡OrdIsoErankU⁡d⁡∅∈har⁡𝒫X
66 37 63 65 sylancr ⊢d∈S→dom⁡OrdIsoErankU⁡d⁡∅∈har⁡𝒫X
67 2 hsmexlem7 ⊢H⁡∅=har⁡𝒫X
68 66 67 eleqtrrdi ⊢d∈S→dom⁡OrdIsoErankU⁡d⁡∅∈H⁡∅
69 68 rgen ⊢∀d∈Sdom⁡OrdIsoErankU⁡d⁡∅∈H⁡∅
70 nfra1 ⊢Ⅎd∀d∈Sdom⁡OrdIsoErankU⁡d⁡e∈H⁡e
71 nfv ⊢Ⅎde∈ω
72 70 71 nfan ⊢Ⅎd∀d∈Sdom⁡OrdIsoErankU⁡d⁡e∈H⁡e∧e∈ω
73 3 ituniiun ⊢d∈V→U⁡d⁡suc⁡e=⋃f∈dU⁡f⁡e
74 73 elv ⊢U⁡d⁡suc⁡e=⋃f∈dU⁡f⁡e
75 74 imaeq2i ⊢rankU⁡d⁡suc⁡e=rank⋃f∈dU⁡f⁡e
76 imaiun ⊢rank⋃f∈dU⁡f⁡e=⋃f∈drankU⁡f⁡e
77 75 76 eqtri ⊢rankU⁡d⁡suc⁡e=⋃f∈drankU⁡f⁡e
78 oieq2 ⊢rankU⁡d⁡suc⁡e=⋃f∈drankU⁡f⁡e→OrdIsoErankU⁡d⁡suc⁡e=OrdIsoE⋃f∈drankU⁡f⁡e
79 77 78 ax-mp ⊢OrdIsoErankU⁡d⁡suc⁡e=OrdIsoE⋃f∈drankU⁡f⁡e
80 79 dmeqi ⊢dom⁡OrdIsoErankU⁡d⁡suc⁡e=dom⁡OrdIsoE⋃f∈drankU⁡f⁡e
81 60 ad2antll ⊢∀d∈Sdom⁡OrdIsoErankU⁡d⁡e∈H⁡e∧e∈ω∧d∈S→d≼*X
82 2 hsmexlem9 ⊢e∈ω→H⁡e∈On
83 82 ad2antrl ⊢∀d∈Sdom⁡OrdIsoErankU⁡d⁡e∈H⁡e∧e∈ω∧d∈S→H⁡e∈On
84 fveq2 ⊢d=f→U⁡d=U⁡f
85 84 fveq1d ⊢d=f→U⁡d⁡e=U⁡f⁡e
86 85 imaeq2d ⊢d=f→rankU⁡d⁡e=rankU⁡f⁡e
87 oieq2 ⊢rankU⁡d⁡e=rankU⁡f⁡e→OrdIsoErankU⁡d⁡e=OrdIsoErankU⁡f⁡e
88 86 87 syl ⊢d=f→OrdIsoErankU⁡d⁡e=OrdIsoErankU⁡f⁡e
89 88 dmeqd ⊢d=f→dom⁡OrdIsoErankU⁡d⁡e=dom⁡OrdIsoErankU⁡f⁡e
90 89 eleq1d ⊢d=f→dom⁡OrdIsoErankU⁡d⁡e∈H⁡e↔dom⁡OrdIsoErankU⁡f⁡e∈H⁡e
91 simpll ⊢∀d∈Sdom⁡OrdIsoErankU⁡d⁡e∈H⁡e∧e∈ω∧d∈S∧f∈d→∀d∈Sdom⁡OrdIsoErankU⁡d⁡e∈H⁡e
92 4 ssrab3 ⊢S⊆⋃R1On
93 92 sseli ⊢d∈S→d∈⋃R1On
94 r1elssi ⊢d∈⋃R1On→d⊆⋃R1On
95 93 94 syl ⊢d∈S→d⊆⋃R1On
96 95 sselda ⊢d∈S∧f∈d→f∈⋃R1On
97 snssi ⊢f∈d→f⊆d
98 43 tcss ⊢f⊆d→TC⁡f⊆TC⁡d
99 97 98 syl ⊢f∈d→TC⁡f⊆TC⁡d
100 51 tcel ⊢d∈d→TC⁡d⊆TC⁡d
101 54 100 mp1i ⊢f∈d→TC⁡d⊆TC⁡d
102 99 101 sstrd ⊢f∈d→TC⁡f⊆TC⁡d
103 ssralv ⊢TC⁡f⊆TC⁡d→∀b∈TC⁡db≼X→∀b∈TC⁡fb≼X
104 102 103 syl ⊢f∈d→∀b∈TC⁡db≼X→∀b∈TC⁡fb≼X
105 50 104 mpan9 ⊢d∈S∧f∈d→∀b∈TC⁡fb≼X
106 sneq ⊢a=f→a=f
107 106 fveq2d ⊢a=f→TC⁡a=TC⁡f
108 107 raleqdv ⊢a=f→∀b∈TC⁡ab≼X↔∀b∈TC⁡fb≼X
109 108 4 elrab2 ⊢f∈S↔f∈⋃R1On∧∀b∈TC⁡fb≼X
110 96 105 109 sylanbrc ⊢d∈S∧f∈d→f∈S
111 110 adantll ⊢e∈ω∧d∈S∧f∈d→f∈S
112 111 adantll ⊢∀d∈Sdom⁡OrdIsoErankU⁡d⁡e∈H⁡e∧e∈ω∧d∈S∧f∈d→f∈S
113 90 91 112 rspcdva ⊢∀d∈Sdom⁡OrdIsoErankU⁡d⁡e∈H⁡e∧e∈ω∧d∈S∧f∈d→dom⁡OrdIsoErankU⁡f⁡e∈H⁡e
114 imassrn ⊢rankU⁡f⁡e⊆ran⁡rank
115 114 36 sstri ⊢rankU⁡f⁡e⊆On
116 fvex ⊢U⁡f⁡e∈V
117 116 funimaex ⊢Fun⁡rank→rankU⁡f⁡e∈V
118 42 117 ax-mp ⊢rankU⁡f⁡e∈V
119 118 elpw ⊢rankU⁡f⁡e∈𝒫On↔rankU⁡f⁡e⊆On
120 115 119 mpbir ⊢rankU⁡f⁡e∈𝒫On
121 113 120 jctil ⊢∀d∈Sdom⁡OrdIsoErankU⁡d⁡e∈H⁡e∧e∈ω∧d∈S∧f∈d→rankU⁡f⁡e∈𝒫On∧dom⁡OrdIsoErankU⁡f⁡e∈H⁡e
122 121 ralrimiva ⊢∀d∈Sdom⁡OrdIsoErankU⁡d⁡e∈H⁡e∧e∈ω∧d∈S→∀f∈drankU⁡f⁡e∈𝒫On∧dom⁡OrdIsoErankU⁡f⁡e∈H⁡e
123 eqid ⊢OrdIsoErankU⁡f⁡e=OrdIsoErankU⁡f⁡e
124 eqid ⊢OrdIsoE⋃f∈drankU⁡f⁡e=OrdIsoE⋃f∈drankU⁡f⁡e
125 123 124 hsmexlem3 ⊢d≼*X∧H⁡e∈On∧∀f∈drankU⁡f⁡e∈𝒫On∧dom⁡OrdIsoErankU⁡f⁡e∈H⁡e→dom⁡OrdIsoE⋃f∈drankU⁡f⁡e∈har⁡𝒫X×H⁡e
126 81 83 122 125 syl21anc ⊢∀d∈Sdom⁡OrdIsoErankU⁡d⁡e∈H⁡e∧e∈ω∧d∈S→dom⁡OrdIsoE⋃f∈drankU⁡f⁡e∈har⁡𝒫X×H⁡e
127 80 126 eqeltrid ⊢∀d∈Sdom⁡OrdIsoErankU⁡d⁡e∈H⁡e∧e∈ω∧d∈S→dom⁡OrdIsoErankU⁡d⁡suc⁡e∈har⁡𝒫X×H⁡e
128 2 hsmexlem8 ⊢e∈ω→H⁡suc⁡e=har⁡𝒫X×H⁡e
129 128 ad2antrl ⊢∀d∈Sdom⁡OrdIsoErankU⁡d⁡e∈H⁡e∧e∈ω∧d∈S→H⁡suc⁡e=har⁡𝒫X×H⁡e
130 127 129 eleqtrrd ⊢∀d∈Sdom⁡OrdIsoErankU⁡d⁡e∈H⁡e∧e∈ω∧d∈S→dom⁡OrdIsoErankU⁡d⁡suc⁡e∈H⁡suc⁡e
131 130 expr ⊢∀d∈Sdom⁡OrdIsoErankU⁡d⁡e∈H⁡e∧e∈ω→d∈S→dom⁡OrdIsoErankU⁡d⁡suc⁡e∈H⁡suc⁡e
132 72 131 ralrimi ⊢∀d∈Sdom⁡OrdIsoErankU⁡d⁡e∈H⁡e∧e∈ω→∀d∈Sdom⁡OrdIsoErankU⁡d⁡suc⁡e∈H⁡suc⁡e
133 132 expcom ⊢e∈ω→∀d∈Sdom⁡OrdIsoErankU⁡d⁡e∈H⁡e→∀d∈Sdom⁡OrdIsoErankU⁡d⁡suc⁡e∈H⁡suc⁡e
134 14 23 32 69 133 finds1 ⊢c∈ω→∀d∈Sdom⁡O∈H⁡c
135 134 r19.21bi ⊢c∈ω∧d∈S→dom⁡O∈H⁡c