Metamath Proof Explorer

Theorem tfisg

Description: A closed form of tfis . (Contributed by Scott Fenton, 8-Jun-2011)

Ref Expression
Assertion tfisg ⊢ ∀ x ∈ On ∀ y ∈ x [˙y / x]˙ φ → φ → ∀ x ∈ On φ

Proof

Step Hyp Ref Expression
1 ssrab2 ⊢ x ∈ On | φ ⊆ On
2 dfss3 ⊢ z ⊆ x ∈ On | φ ↔ ∀ y ∈ z y ∈ x ∈ On | φ
3 nfcv ⊢ Ⅎ _ x On
4 3 elrabsf ⊢ y ∈ x ∈ On | φ ↔ y ∈ On ∧ [˙y / x]˙ φ
5 4 simprbi ⊢ y ∈ x ∈ On | φ → [˙y / x]˙ φ
6 5 ralimi ⊢ ∀ y ∈ z y ∈ x ∈ On | φ → ∀ y ∈ z [˙y / x]˙ φ
7 2 6 sylbi ⊢ z ⊆ x ∈ On | φ → ∀ y ∈ z [˙y / x]˙ φ
8 nfcv ⊢ Ⅎ _ x z
9 nfsbc1v ⊢ Ⅎ x [˙y / x]˙ φ
10 8 9 nfralw ⊢ Ⅎ x ∀ y ∈ z [˙y / x]˙ φ
11 nfsbc1v ⊢ Ⅎ x [˙z / x]˙ φ
12 10 11 nfim ⊢ Ⅎ x ∀ y ∈ z [˙y / x]˙ φ → [˙z / x]˙ φ
13 raleq ⊢ x = z → ∀ y ∈ x [˙y / x]˙ φ ↔ ∀ y ∈ z [˙y / x]˙ φ
14 sbceq1a ⊢ x = z → φ ↔ [˙z / x]˙ φ
15 13 14 imbi12d ⊢ x = z → ∀ y ∈ x [˙y / x]˙ φ → φ ↔ ∀ y ∈ z [˙y / x]˙ φ → [˙z / x]˙ φ
16 12 15 rspc ⊢ z ∈ On → ∀ x ∈ On ∀ y ∈ x [˙y / x]˙ φ → φ → ∀ y ∈ z [˙y / x]˙ φ → [˙z / x]˙ φ
17 16 impcom ⊢ ∀ x ∈ On ∀ y ∈ x [˙y / x]˙ φ → φ ∧ z ∈ On → ∀ y ∈ z [˙y / x]˙ φ → [˙z / x]˙ φ
18 7 17 syl5 ⊢ ∀ x ∈ On ∀ y ∈ x [˙y / x]˙ φ → φ ∧ z ∈ On → z ⊆ x ∈ On | φ → [˙z / x]˙ φ
19 simpr ⊢ ∀ x ∈ On ∀ y ∈ x [˙y / x]˙ φ → φ ∧ z ∈ On → z ∈ On
20 18 19 jctild ⊢ ∀ x ∈ On ∀ y ∈ x [˙y / x]˙ φ → φ ∧ z ∈ On → z ⊆ x ∈ On | φ → z ∈ On ∧ [˙z / x]˙ φ
21 3 elrabsf ⊢ z ∈ x ∈ On | φ ↔ z ∈ On ∧ [˙z / x]˙ φ
22 20 21 imbitrrdi ⊢ ∀ x ∈ On ∀ y ∈ x [˙y / x]˙ φ → φ ∧ z ∈ On → z ⊆ x ∈ On | φ → z ∈ x ∈ On | φ
23 22 ralrimiva ⊢ ∀ x ∈ On ∀ y ∈ x [˙y / x]˙ φ → φ → ∀ z ∈ On z ⊆ x ∈ On | φ → z ∈ x ∈ On | φ
24 tfi ⊢ x ∈ On | φ ⊆ On ∧ ∀ z ∈ On z ⊆ x ∈ On | φ → z ∈ x ∈ On | φ → x ∈ On | φ = On
25 1 23 24 sylancr ⊢ ∀ x ∈ On ∀ y ∈ x [˙y / x]˙ φ → φ → x ∈ On | φ = On
26 25 eqcomd ⊢ ∀ x ∈ On ∀ y ∈ x [˙y / x]˙ φ → φ → On = x ∈ On | φ
27 rabid2 ⊢ On = x ∈ On | φ ↔ ∀ x ∈ On φ
28 26 27 sylib ⊢ ∀ x ∈ On ∀ y ∈ x [˙y / x]˙ φ → φ → ∀ x ∈ On φ