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 𝜑 )