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

Metamath Proof Explorer

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