Metamath Proof Explorer

Theorem hsmexlem6

Description: Lemma for hsmex . (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 hsmexlem6 ⊢ S ∈ V

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 fvex ⊢ R1 ⁡ har ⁡ 𝒫 ω × ⋃ ran ⁡ H ∈ V
7 1 2 3 4 5 hsmexlem5 ⊢ d ∈ S → rank ⁡ d ∈ har ⁡ 𝒫 ω × ⋃ ran ⁡ H
8 4 ssrab3 ⊢ S ⊆ ⋃ R1 On
9 8 sseli ⊢ d ∈ S → d ∈ ⋃ R1 On
10 harcl ⊢ har ⁡ 𝒫 ω × ⋃ ran ⁡ H ∈ On
11 r1fnon ⊢ R1 Fn On
12 11 fndmi ⊢ dom ⁡ R1 = On
13 10 12 eleqtrri ⊢ har ⁡ 𝒫 ω × ⋃ ran ⁡ H ∈ dom ⁡ R1
14 rankr1ag ⊢ d ∈ ⋃ R1 On ∧ har ⁡ 𝒫 ω × ⋃ ran ⁡ H ∈ dom ⁡ R1 → d ∈ R1 ⁡ har ⁡ 𝒫 ω × ⋃ ran ⁡ H ↔ rank ⁡ d ∈ har ⁡ 𝒫 ω × ⋃ ran ⁡ H
15 9 13 14 sylancl ⊢ d ∈ S → d ∈ R1 ⁡ har ⁡ 𝒫 ω × ⋃ ran ⁡ H ↔ rank ⁡ d ∈ har ⁡ 𝒫 ω × ⋃ ran ⁡ H
16 7 15 mpbird ⊢ d ∈ S → d ∈ R1 ⁡ har ⁡ 𝒫 ω × ⋃ ran ⁡ H
17 16 ssriv ⊢ S ⊆ R1 ⁡ har ⁡ 𝒫 ω × ⋃ ran ⁡ H
18 6 17 ssexi ⊢ S ∈ V