Metamath Proof Explorer

Theorem hsmexlem5

Description: Lemma for hsmex . Combining the above constraints, along with itunitc and tcrank , gives an effective constraint on the rank of S . (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 hsmexlem5 ⊢ d ∈ S → rank ⁡ d ∈ har ⁡ 𝒫 ω × ⋃ ran ⁡ H

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 4 ssrab3 ⊢ S ⊆ ⋃ R1 On
7 6 sseli ⊢ d ∈ S → d ∈ ⋃ R1 On
8 tcrank ⊢ d ∈ ⋃ R1 On → rank ⁡ d = rank TC ⁡ d
9 7 8 syl ⊢ d ∈ S → rank ⁡ d = rank TC ⁡ d
10 3 itunitc ⊢ TC ⁡ d = ⋃ ran ⁡ U ⁡ d
11 3 itunifn ⊢ d ∈ S → U ⁡ d Fn ω
12 fniunfv ⊢ U ⁡ d Fn ω → ⋃ c ∈ ω U ⁡ d ⁡ c = ⋃ ran ⁡ U ⁡ d
13 11 12 syl ⊢ d ∈ S → ⋃ c ∈ ω U ⁡ d ⁡ c = ⋃ ran ⁡ U ⁡ d
14 10 13 eqtr4id ⊢ d ∈ S → TC ⁡ d = ⋃ c ∈ ω U ⁡ d ⁡ c
15 14 imaeq2d ⊢ d ∈ S → rank TC ⁡ d = rank ⋃ c ∈ ω U ⁡ d ⁡ c
16 imaiun ⊢ rank ⋃ c ∈ ω U ⁡ d ⁡ c = ⋃ c ∈ ω rank U ⁡ d ⁡ c
17 16 a1i ⊢ d ∈ S → rank ⋃ c ∈ ω U ⁡ d ⁡ c = ⋃ c ∈ ω rank U ⁡ d ⁡ c
18 9 15 17 3eqtrd ⊢ d ∈ S → rank ⁡ d = ⋃ c ∈ ω rank U ⁡ d ⁡ c
19 dmresi ⊢ dom ⁡ I ↾ ⋃ c ∈ ω rank U ⁡ d ⁡ c = ⋃ c ∈ ω rank U ⁡ d ⁡ c
20 18 19 eqtr4di ⊢ d ∈ S → rank ⁡ d = dom ⁡ I ↾ ⋃ c ∈ ω rank U ⁡ d ⁡ c
21 rankon ⊢ rank ⁡ d ∈ On
22 18 21 eqeltrrdi ⊢ d ∈ S → ⋃ c ∈ ω rank U ⁡ d ⁡ c ∈ On
23 eloni ⊢ ⋃ c ∈ ω rank U ⁡ d ⁡ c ∈ On → Ord ⁡ ⋃ c ∈ ω rank U ⁡ d ⁡ c
24 oiid ⊢ Ord ⁡ ⋃ c ∈ ω rank U ⁡ d ⁡ c → OrdIso E ⋃ c ∈ ω rank U ⁡ d ⁡ c = I ↾ ⋃ c ∈ ω rank U ⁡ d ⁡ c
25 22 23 24 3syl ⊢ d ∈ S → OrdIso E ⋃ c ∈ ω rank U ⁡ d ⁡ c = I ↾ ⋃ c ∈ ω rank U ⁡ d ⁡ c
26 25 dmeqd ⊢ d ∈ S → dom ⁡ OrdIso E ⋃ c ∈ ω rank U ⁡ d ⁡ c = dom ⁡ I ↾ ⋃ c ∈ ω rank U ⁡ d ⁡ c
27 20 26 eqtr4d ⊢ d ∈ S → rank ⁡ d = dom ⁡ OrdIso E ⋃ c ∈ ω rank U ⁡ d ⁡ c
28 omex ⊢ ω ∈ V
29 wdomref ⊢ ω ∈ V → ω ≼ * ω
30 28 29 mp1i ⊢ d ∈ S → ω ≼ * ω
31 frfnom ⊢ rec ⁡ z ∈ V ⟼ har ⁡ 𝒫 X × z har ⁡ 𝒫 X ↾ ω Fn ω
32 2 fneq1i ⊢ H Fn ω ↔ rec ⁡ z ∈ V ⟼ har ⁡ 𝒫 X × z har ⁡ 𝒫 X ↾ ω Fn ω
33 31 32 mpbir ⊢ H Fn ω
34 fniunfv ⊢ H Fn ω → ⋃ a ∈ ω H ⁡ a = ⋃ ran ⁡ H
35 33 34 ax-mp ⊢ ⋃ a ∈ ω H ⁡ a = ⋃ ran ⁡ H
36 iunon ⊢ ω ∈ V ∧ ∀ a ∈ ω H ⁡ a ∈ On → ⋃ a ∈ ω H ⁡ a ∈ On
37 28 36 mpan ⊢ ∀ a ∈ ω H ⁡ a ∈ On → ⋃ a ∈ ω H ⁡ a ∈ On
38 2 hsmexlem9 ⊢ a ∈ ω → H ⁡ a ∈ On
39 37 38 mprg ⊢ ⋃ a ∈ ω H ⁡ a ∈ On
40 35 39 eqeltrri ⊢ ⋃ ran ⁡ H ∈ On
41 40 a1i ⊢ d ∈ S → ⋃ ran ⁡ H ∈ On
42 fvssunirn ⊢ H ⁡ c ⊆ ⋃ ran ⁡ H
43 eqid ⊢ OrdIso E rank U ⁡ d ⁡ c = OrdIso E rank U ⁡ d ⁡ c
44 1 2 3 4 43 hsmexlem4 ⊢ c ∈ ω ∧ d ∈ S → dom ⁡ OrdIso E rank U ⁡ d ⁡ c ∈ H ⁡ c
45 44 ancoms ⊢ d ∈ S ∧ c ∈ ω → dom ⁡ OrdIso E rank U ⁡ d ⁡ c ∈ H ⁡ c
46 42 45 sseldi ⊢ d ∈ S ∧ c ∈ ω → dom ⁡ OrdIso E rank U ⁡ d ⁡ c ∈ ⋃ ran ⁡ H
47 imassrn ⊢ rank U ⁡ d ⁡ c ⊆ ran ⁡ rank
48 rankf ⊢ rank : ⋃ R1 On ⟶ On
49 frn ⊢ rank : ⋃ R1 On ⟶ On → ran ⁡ rank ⊆ On
50 48 49 ax-mp ⊢ ran ⁡ rank ⊆ On
51 47 50 sstri ⊢ rank U ⁡ d ⁡ c ⊆ On
52 ffun ⊢ rank : ⋃ R1 On ⟶ On → Fun ⁡ rank
53 fvex ⊢ U ⁡ d ⁡ c ∈ V
54 53 funimaex ⊢ Fun ⁡ rank → rank U ⁡ d ⁡ c ∈ V
55 48 52 54 mp2b ⊢ rank U ⁡ d ⁡ c ∈ V
56 55 elpw ⊢ rank U ⁡ d ⁡ c ∈ 𝒫 On ↔ rank U ⁡ d ⁡ c ⊆ On
57 51 56 mpbir ⊢ rank U ⁡ d ⁡ c ∈ 𝒫 On
58 46 57 jctil ⊢ d ∈ S ∧ c ∈ ω → rank U ⁡ d ⁡ c ∈ 𝒫 On ∧ dom ⁡ OrdIso E rank U ⁡ d ⁡ c ∈ ⋃ ran ⁡ H
59 58 ralrimiva ⊢ d ∈ S → ∀ c ∈ ω rank U ⁡ d ⁡ c ∈ 𝒫 On ∧ dom ⁡ OrdIso E rank U ⁡ d ⁡ c ∈ ⋃ ran ⁡ H
60 eqid ⊢ OrdIso E ⋃ c ∈ ω rank U ⁡ d ⁡ c = OrdIso E ⋃ c ∈ ω rank U ⁡ d ⁡ c
61 43 60 hsmexlem3 ⊢ ω ≼ * ω ∧ ⋃ ran ⁡ H ∈ On ∧ ∀ c ∈ ω rank U ⁡ d ⁡ c ∈ 𝒫 On ∧ dom ⁡ OrdIso E rank U ⁡ d ⁡ c ∈ ⋃ ran ⁡ H → dom ⁡ OrdIso E ⋃ c ∈ ω rank U ⁡ d ⁡ c ∈ har ⁡ 𝒫 ω × ⋃ ran ⁡ H
62 30 41 59 61 syl21anc ⊢ d ∈ S → dom ⁡ OrdIso E ⋃ c ∈ ω rank U ⁡ d ⁡ c ∈ har ⁡ 𝒫 ω × ⋃ ran ⁡ H
63 27 62 eqeltrd ⊢ d ∈ S → rank ⁡ d ∈ har ⁡ 𝒫 ω × ⋃ ran ⁡ H