Metamath Proof Explorer


Theorem hartogslem2

Description: Lemma for hartogs . (Contributed by Mario Carneiro, 14-Jan-2013)

Ref Expression
Hypotheses hartogslem.2 𝐹 = { ⟨ 𝑟 , 𝑦 ⟩ ∣ ( ( ( dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟 ) ⊆ 𝑟𝑟 ⊆ ( dom 𝑟 × dom 𝑟 ) ) ∧ ( 𝑟 ∖ I ) We dom 𝑟 ) ∧ 𝑦 = dom OrdIso ( ( 𝑟 ∖ I ) , dom 𝑟 ) ) }
hartogslem.3 𝑅 = { ⟨ 𝑠 , 𝑡 ⟩ ∣ ∃ 𝑤𝑦𝑧𝑦 ( ( 𝑠 = ( 𝑓𝑤 ) ∧ 𝑡 = ( 𝑓𝑧 ) ) ∧ 𝑤 E 𝑧 ) }
Assertion hartogslem2 ( 𝐴𝑉 → { 𝑥 ∈ On ∣ 𝑥𝐴 } ∈ V )

Proof

Step Hyp Ref Expression
1 hartogslem.2 𝐹 = { ⟨ 𝑟 , 𝑦 ⟩ ∣ ( ( ( dom 𝑟𝐴 ∧ ( I ↾ dom 𝑟 ) ⊆ 𝑟𝑟 ⊆ ( dom 𝑟 × dom 𝑟 ) ) ∧ ( 𝑟 ∖ I ) We dom 𝑟 ) ∧ 𝑦 = dom OrdIso ( ( 𝑟 ∖ I ) , dom 𝑟 ) ) }
2 hartogslem.3 𝑅 = { ⟨ 𝑠 , 𝑡 ⟩ ∣ ∃ 𝑤𝑦𝑧𝑦 ( ( 𝑠 = ( 𝑓𝑤 ) ∧ 𝑡 = ( 𝑓𝑧 ) ) ∧ 𝑤 E 𝑧 ) }
3 1 2 hartogslem1 ( dom 𝐹 ⊆ 𝒫 ( 𝐴 × 𝐴 ) ∧ Fun 𝐹 ∧ ( 𝐴𝑉 → ran 𝐹 = { 𝑥 ∈ On ∣ 𝑥𝐴 } ) )
4 3 simp3i ( 𝐴𝑉 → ran 𝐹 = { 𝑥 ∈ On ∣ 𝑥𝐴 } )
5 3 simp2i Fun 𝐹
6 3 simp1i dom 𝐹 ⊆ 𝒫 ( 𝐴 × 𝐴 )
7 sqxpexg ( 𝐴𝑉 → ( 𝐴 × 𝐴 ) ∈ V )
8 7 pwexd ( 𝐴𝑉 → 𝒫 ( 𝐴 × 𝐴 ) ∈ V )
9 ssexg ( ( dom 𝐹 ⊆ 𝒫 ( 𝐴 × 𝐴 ) ∧ 𝒫 ( 𝐴 × 𝐴 ) ∈ V ) → dom 𝐹 ∈ V )
10 6 8 9 sylancr ( 𝐴𝑉 → dom 𝐹 ∈ V )
11 funex ( ( Fun 𝐹 ∧ dom 𝐹 ∈ V ) → 𝐹 ∈ V )
12 5 10 11 sylancr ( 𝐴𝑉𝐹 ∈ V )
13 rnexg ( 𝐹 ∈ V → ran 𝐹 ∈ V )
14 12 13 syl ( 𝐴𝑉 → ran 𝐹 ∈ V )
15 4 14 eqeltrrd ( 𝐴𝑉 → { 𝑥 ∈ On ∣ 𝑥𝐴 } ∈ V )