Theorem hsmexlem6

Description: Lemma for hsmex . (Contributed by Stefan O'Rear, 14-Feb-2015)

	Ref	Expression
Hypotheses	hsmexlem4.x	⊢ 𝑋 ∈ V
	hsmexlem4.h	⊢ 𝐻 = ( rec ( ( 𝑧 ∈ V ↦ ( har ‘ 𝒫 ( 𝑋 × 𝑧 ) ) ) , ( har ‘ 𝒫 𝑋 ) ) ↾ ω )
	hsmexlem4.u	⊢ 𝑈 = ( 𝑥 ∈ V ↦ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , 𝑥 ) ↾ ω ) )
	hsmexlem4.s	⊢ 𝑆 = { 𝑎 ∈ ∪ ( 𝑅1 “ On ) ∣ ∀ 𝑏 ∈ ( TC ‘ { 𝑎 } ) 𝑏 ≼ 𝑋 }
	hsmexlem4.o	⊢ 𝑂 = OrdIso ( E , ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ 𝑐 ) ) )
Assertion	hsmexlem6	⊢ 𝑆 ∈ V

Proof

Step	Hyp	Ref	Expression
1		hsmexlem4.x	⊢ 𝑋 ∈ V
2		hsmexlem4.h	⊢ 𝐻 = ( rec ( ( 𝑧 ∈ V ↦ ( har ‘ 𝒫 ( 𝑋 × 𝑧 ) ) ) , ( har ‘ 𝒫 𝑋 ) ) ↾ ω )
3		hsmexlem4.u	⊢ 𝑈 = ( 𝑥 ∈ V ↦ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , 𝑥 ) ↾ ω ) )
4		hsmexlem4.s	⊢ 𝑆 = { 𝑎 ∈ ∪ ( 𝑅1 “ On ) ∣ ∀ 𝑏 ∈ ( TC ‘ { 𝑎 } ) 𝑏 ≼ 𝑋 }
5		hsmexlem4.o	⊢ 𝑂 = OrdIso ( E , ( rank “ ( ( 𝑈 ‘ 𝑑 ) ‘ 𝑐 ) ) )
6		fvex	⊢ ( 𝑅1 ‘ ( har ‘ 𝒫 ( ω × ∪ ran 𝐻 ) ) ) ∈ V
7	1 2 3 4 5	hsmexlem5	⊢ ( 𝑑 ∈ 𝑆 → ( rank ‘ 𝑑 ) ∈ ( har ‘ 𝒫 ( ω × ∪ ran 𝐻 ) ) )
8	4	ssrab3	⊢ 𝑆 ⊆ ∪ ( 𝑅1 “ On )
9	8	sseli	⊢ ( 𝑑 ∈ 𝑆 → 𝑑 ∈ ∪ ( 𝑅1 “ On ) )
10		harcl	⊢ ( har ‘ 𝒫 ( ω × ∪ ran 𝐻 ) ) ∈ On
11		r1fnon	⊢ 𝑅1 Fn On
12	11	fndmi	⊢ dom 𝑅1 = On
13	10 12	eleqtrri	⊢ ( har ‘ 𝒫 ( ω × ∪ ran 𝐻 ) ) ∈ dom 𝑅1
14		rankr1ag	⊢ ( ( 𝑑 ∈ ∪ ( 𝑅1 “ On ) ∧ ( har ‘ 𝒫 ( ω × ∪ ran 𝐻 ) ) ∈ dom 𝑅1 ) → ( 𝑑 ∈ ( 𝑅1 ‘ ( har ‘ 𝒫 ( ω × ∪ ran 𝐻 ) ) ) ↔ ( rank ‘ 𝑑 ) ∈ ( har ‘ 𝒫 ( ω × ∪ ran 𝐻 ) ) ) )
15	9 13 14	sylancl	⊢ ( 𝑑 ∈ 𝑆 → ( 𝑑 ∈ ( 𝑅1 ‘ ( har ‘ 𝒫 ( ω × ∪ ran 𝐻 ) ) ) ↔ ( rank ‘ 𝑑 ) ∈ ( har ‘ 𝒫 ( ω × ∪ ran 𝐻 ) ) ) )
16	7 15	mpbird	⊢ ( 𝑑 ∈ 𝑆 → 𝑑 ∈ ( 𝑅1 ‘ ( har ‘ 𝒫 ( ω × ∪ ran 𝐻 ) ) ) )
17	16	ssriv	⊢ 𝑆 ⊆ ( 𝑅1 ‘ ( har ‘ 𝒫 ( ω × ∪ ran 𝐻 ) ) )
18	6 17	ssexi	⊢ 𝑆 ∈ V