Theorem tz9.12lem1

Description: Lemma for tz9.12 . (Contributed by NM, 22-Sep-2003) (Revised by Mario Carneiro, 11-Sep-2015)

	Ref	Expression
Hypotheses	tz9.12lem.1	⊢ 𝐴 ∈ V
	tz9.12lem.2	⊢ 𝐹 = ( 𝑧 ∈ V ↦ ∩ { 𝑣 ∈ On ∣ 𝑧 ∈ ( 𝑅1 ‘ 𝑣 ) } )
Assertion	tz9.12lem1	⊢ ( 𝐹 “ 𝐴 ) ⊆ On

Proof

Step	Hyp	Ref	Expression
1		tz9.12lem.1	⊢ 𝐴 ∈ V
2		tz9.12lem.2	⊢ 𝐹 = ( 𝑧 ∈ V ↦ ∩ { 𝑣 ∈ On ∣ 𝑧 ∈ ( 𝑅1 ‘ 𝑣 ) } )
3		imassrn	⊢ ( 𝐹 “ 𝐴 ) ⊆ ran 𝐹
4	2	rnmpt	⊢ ran 𝐹 = { 𝑥 ∣ ∃ 𝑧 ∈ V 𝑥 = ∩ { 𝑣 ∈ On ∣ 𝑧 ∈ ( 𝑅1 ‘ 𝑣 ) } }
5		id	⊢ ( 𝑥 = ∩ { 𝑣 ∈ On ∣ 𝑧 ∈ ( 𝑅1 ‘ 𝑣 ) } → 𝑥 = ∩ { 𝑣 ∈ On ∣ 𝑧 ∈ ( 𝑅1 ‘ 𝑣 ) } )
6		ssrab2	⊢ { 𝑣 ∈ On ∣ 𝑧 ∈ ( 𝑅1 ‘ 𝑣 ) } ⊆ On
7		eqvisset	⊢ ( 𝑥 = ∩ { 𝑣 ∈ On ∣ 𝑧 ∈ ( 𝑅1 ‘ 𝑣 ) } → ∩ { 𝑣 ∈ On ∣ 𝑧 ∈ ( 𝑅1 ‘ 𝑣 ) } ∈ V )
8		intex	⊢ ( { 𝑣 ∈ On ∣ 𝑧 ∈ ( 𝑅1 ‘ 𝑣 ) } ≠ ∅ ↔ ∩ { 𝑣 ∈ On ∣ 𝑧 ∈ ( 𝑅1 ‘ 𝑣 ) } ∈ V )
9	7 8	sylibr	⊢ ( 𝑥 = ∩ { 𝑣 ∈ On ∣ 𝑧 ∈ ( 𝑅1 ‘ 𝑣 ) } → { 𝑣 ∈ On ∣ 𝑧 ∈ ( 𝑅1 ‘ 𝑣 ) } ≠ ∅ )
10		oninton	⊢ ( ( { 𝑣 ∈ On ∣ 𝑧 ∈ ( 𝑅1 ‘ 𝑣 ) } ⊆ On ∧ { 𝑣 ∈ On ∣ 𝑧 ∈ ( 𝑅1 ‘ 𝑣 ) } ≠ ∅ ) → ∩ { 𝑣 ∈ On ∣ 𝑧 ∈ ( 𝑅1 ‘ 𝑣 ) } ∈ On )
11	6 9 10	sylancr	⊢ ( 𝑥 = ∩ { 𝑣 ∈ On ∣ 𝑧 ∈ ( 𝑅1 ‘ 𝑣 ) } → ∩ { 𝑣 ∈ On ∣ 𝑧 ∈ ( 𝑅1 ‘ 𝑣 ) } ∈ On )
12	5 11	eqeltrd	⊢ ( 𝑥 = ∩ { 𝑣 ∈ On ∣ 𝑧 ∈ ( 𝑅1 ‘ 𝑣 ) } → 𝑥 ∈ On )
13	12	rexlimivw	⊢ ( ∃ 𝑧 ∈ V 𝑥 = ∩ { 𝑣 ∈ On ∣ 𝑧 ∈ ( 𝑅1 ‘ 𝑣 ) } → 𝑥 ∈ On )
14	13	abssi	⊢ { 𝑥 ∣ ∃ 𝑧 ∈ V 𝑥 = ∩ { 𝑣 ∈ On ∣ 𝑧 ∈ ( 𝑅1 ‘ 𝑣 ) } } ⊆ On
15	4 14	eqsstri	⊢ ran 𝐹 ⊆ On
16	3 15	sstri	⊢ ( 𝐹 “ 𝐴 ) ⊆ On