Metamath Proof Explorer


Theorem tfisg

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

Ref Expression
Assertion tfisg ( ∀ 𝑥 ∈ On ( ∀ 𝑦𝑥 [ 𝑦 / 𝑥 ] 𝜑𝜑 ) → ∀ 𝑥 ∈ On 𝜑 )

Proof

Step Hyp Ref Expression
1 ssrab2 { 𝑥 ∈ On ∣ 𝜑 } ⊆ On
2 dfss3 ( 𝑧 ⊆ { 𝑥 ∈ On ∣ 𝜑 } ↔ ∀ 𝑦𝑧 𝑦 ∈ { 𝑥 ∈ On ∣ 𝜑 } )
3 nfcv 𝑥 On
4 3 elrabsf ( 𝑦 ∈ { 𝑥 ∈ On ∣ 𝜑 } ↔ ( 𝑦 ∈ On ∧ [ 𝑦 / 𝑥 ] 𝜑 ) )
5 4 simprbi ( 𝑦 ∈ { 𝑥 ∈ On ∣ 𝜑 } → [ 𝑦 / 𝑥 ] 𝜑 )
6 5 ralimi ( ∀ 𝑦𝑧 𝑦 ∈ { 𝑥 ∈ On ∣ 𝜑 } → ∀ 𝑦𝑧 [ 𝑦 / 𝑥 ] 𝜑 )
7 2 6 sylbi ( 𝑧 ⊆ { 𝑥 ∈ On ∣ 𝜑 } → ∀ 𝑦𝑧 [ 𝑦 / 𝑥 ] 𝜑 )
8 nfcv 𝑥 𝑧
9 nfsbc1v 𝑥 [ 𝑦 / 𝑥 ] 𝜑
10 8 9 nfralw 𝑥𝑦𝑧 [ 𝑦 / 𝑥 ] 𝜑
11 nfsbc1v 𝑥 [ 𝑧 / 𝑥 ] 𝜑
12 10 11 nfim 𝑥 ( ∀ 𝑦𝑧 [ 𝑦 / 𝑥 ] 𝜑[ 𝑧 / 𝑥 ] 𝜑 )
13 raleq ( 𝑥 = 𝑧 → ( ∀ 𝑦𝑥 [ 𝑦 / 𝑥 ] 𝜑 ↔ ∀ 𝑦𝑧 [ 𝑦 / 𝑥 ] 𝜑 ) )
14 sbceq1a ( 𝑥 = 𝑧 → ( 𝜑[ 𝑧 / 𝑥 ] 𝜑 ) )
15 13 14 imbi12d ( 𝑥 = 𝑧 → ( ( ∀ 𝑦𝑥 [ 𝑦 / 𝑥 ] 𝜑𝜑 ) ↔ ( ∀ 𝑦𝑧 [ 𝑦 / 𝑥 ] 𝜑[ 𝑧 / 𝑥 ] 𝜑 ) ) )
16 12 15 rspc ( 𝑧 ∈ On → ( ∀ 𝑥 ∈ On ( ∀ 𝑦𝑥 [ 𝑦 / 𝑥 ] 𝜑𝜑 ) → ( ∀ 𝑦𝑧 [ 𝑦 / 𝑥 ] 𝜑[ 𝑧 / 𝑥 ] 𝜑 ) ) )
17 16 impcom ( ( ∀ 𝑥 ∈ On ( ∀ 𝑦𝑥 [ 𝑦 / 𝑥 ] 𝜑𝜑 ) ∧ 𝑧 ∈ On ) → ( ∀ 𝑦𝑧 [ 𝑦 / 𝑥 ] 𝜑[ 𝑧 / 𝑥 ] 𝜑 ) )
18 7 17 syl5 ( ( ∀ 𝑥 ∈ On ( ∀ 𝑦𝑥 [ 𝑦 / 𝑥 ] 𝜑𝜑 ) ∧ 𝑧 ∈ On ) → ( 𝑧 ⊆ { 𝑥 ∈ On ∣ 𝜑 } → [ 𝑧 / 𝑥 ] 𝜑 ) )
19 simpr ( ( ∀ 𝑥 ∈ On ( ∀ 𝑦𝑥 [ 𝑦 / 𝑥 ] 𝜑𝜑 ) ∧ 𝑧 ∈ On ) → 𝑧 ∈ On )
20 18 19 jctild ( ( ∀ 𝑥 ∈ On ( ∀ 𝑦𝑥 [ 𝑦 / 𝑥 ] 𝜑𝜑 ) ∧ 𝑧 ∈ On ) → ( 𝑧 ⊆ { 𝑥 ∈ On ∣ 𝜑 } → ( 𝑧 ∈ On ∧ [ 𝑧 / 𝑥 ] 𝜑 ) ) )
21 3 elrabsf ( 𝑧 ∈ { 𝑥 ∈ On ∣ 𝜑 } ↔ ( 𝑧 ∈ On ∧ [ 𝑧 / 𝑥 ] 𝜑 ) )
22 20 21 syl6ibr ( ( ∀ 𝑥 ∈ On ( ∀ 𝑦𝑥 [ 𝑦 / 𝑥 ] 𝜑𝜑 ) ∧ 𝑧 ∈ On ) → ( 𝑧 ⊆ { 𝑥 ∈ On ∣ 𝜑 } → 𝑧 ∈ { 𝑥 ∈ On ∣ 𝜑 } ) )
23 22 ralrimiva ( ∀ 𝑥 ∈ On ( ∀ 𝑦𝑥 [ 𝑦 / 𝑥 ] 𝜑𝜑 ) → ∀ 𝑧 ∈ On ( 𝑧 ⊆ { 𝑥 ∈ On ∣ 𝜑 } → 𝑧 ∈ { 𝑥 ∈ On ∣ 𝜑 } ) )
24 tfi ( ( { 𝑥 ∈ On ∣ 𝜑 } ⊆ On ∧ ∀ 𝑧 ∈ On ( 𝑧 ⊆ { 𝑥 ∈ On ∣ 𝜑 } → 𝑧 ∈ { 𝑥 ∈ On ∣ 𝜑 } ) ) → { 𝑥 ∈ On ∣ 𝜑 } = On )
25 1 23 24 sylancr ( ∀ 𝑥 ∈ On ( ∀ 𝑦𝑥 [ 𝑦 / 𝑥 ] 𝜑𝜑 ) → { 𝑥 ∈ On ∣ 𝜑 } = On )
26 25 eqcomd ( ∀ 𝑥 ∈ On ( ∀ 𝑦𝑥 [ 𝑦 / 𝑥 ] 𝜑𝜑 ) → On = { 𝑥 ∈ On ∣ 𝜑 } )
27 rabid2 ( On = { 𝑥 ∈ On ∣ 𝜑 } ↔ ∀ 𝑥 ∈ On 𝜑 )
28 26 27 sylib ( ∀ 𝑥 ∈ On ( ∀ 𝑦𝑥 [ 𝑦 / 𝑥 ] 𝜑𝜑 ) → ∀ 𝑥 ∈ On 𝜑 )