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 )