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