This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )