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

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 imbitrrdi ⊢ ( ( ∀ 𝑥 ∈ 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 𝜑 )