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 ⊢ A ∈ V
tz9.12lem.2 ⊢ F = z ∈ V ⟼ ⋂ v ∈ On | z ∈ R1 ⁡ v
Assertion tz9.12lem1 ⊢ F A ⊆ On

Proof

Step Hyp Ref Expression
1 tz9.12lem.1 ⊢ A ∈ V
2 tz9.12lem.2 ⊢ F = z ∈ V ⟼ ⋂ v ∈ On | z ∈ R1 ⁡ v
3 imassrn ⊢ F A ⊆ ran ⁡ F
4 2 rnmpt ⊢ ran ⁡ F = x | ∃ z ∈ V x = ⋂ v ∈ On | z ∈ R1 ⁡ v
5 id ⊢ x = ⋂ v ∈ On | z ∈ R1 ⁡ v → x = ⋂ v ∈ On | z ∈ R1 ⁡ v
6 ssrab2 ⊢ v ∈ On | z ∈ R1 ⁡ v ⊆ On
7 eqvisset ⊢ x = ⋂ v ∈ On | z ∈ R1 ⁡ v → ⋂ v ∈ On | z ∈ R1 ⁡ v ∈ V
8 intex ⊢ v ∈ On | z ∈ R1 ⁡ v ≠ ∅ ↔ ⋂ v ∈ On | z ∈ R1 ⁡ v ∈ V
9 7 8 sylibr ⊢ x = ⋂ v ∈ On | z ∈ R1 ⁡ v → v ∈ On | z ∈ R1 ⁡ v ≠ ∅
10 oninton ⊢ v ∈ On | z ∈ R1 ⁡ v ⊆ On ∧ v ∈ On | z ∈ R1 ⁡ v ≠ ∅ → ⋂ v ∈ On | z ∈ R1 ⁡ v ∈ On
11 6 9 10 sylancr ⊢ x = ⋂ v ∈ On | z ∈ R1 ⁡ v → ⋂ v ∈ On | z ∈ R1 ⁡ v ∈ On
12 5 11 eqeltrd ⊢ x = ⋂ v ∈ On | z ∈ R1 ⁡ v → x ∈ On
13 12 rexlimivw ⊢ ∃ z ∈ V x = ⋂ v ∈ On | z ∈ R1 ⁡ v → x ∈ On
14 13 abssi ⊢ x | ∃ z ∈ V x = ⋂ v ∈ On | z ∈ R1 ⁡ v ⊆ On
15 4 14 eqsstri ⊢ ran ⁡ F ⊆ On
16 3 15 sstri ⊢ F A ⊆ On