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×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 hsmexlem6 ⊢S∈V

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 fvex ⊢R1⁡har⁡𝒫ω×⋃ran⁡H∈V
7 1 2 3 4 5 hsmexlem5 ⊢d∈S→rank⁡d∈har⁡𝒫ω×⋃ran⁡H
8 4 ssrab3 ⊢S⊆⋃R1On
9 8 sseli ⊢d∈S→d∈⋃R1On
10 harcl ⊢har⁡𝒫ω×⋃ran⁡H∈On
11 r1fnon ⊢R1FnOn
12 11 fndmi ⊢dom⁡R1=On
13 10 12 eleqtrri ⊢har⁡𝒫ω×⋃ran⁡H∈dom⁡R1
14 rankr1ag ⊢d∈⋃R1On∧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