Metamath Proof Explorer

Theorem tfisg

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

Ref Expression
Assertion tfisg 
|- ( A. x e. On ( A. y e. x [. y / x ]. ph -> ph ) -> A. x e. On ph )

Proof

Step Hyp Ref Expression
1 ssrab2 
 |-  { x e. On | ph } C_ On
2 dfss3 
 |-  ( z C_ { x e. On | ph } <-> A. y e. z y e. { x e. On | ph } )
3 nfcv 
 |-  F/_ x On
4 3 elrabsf 
 |-  ( y e. { x e. On | ph } <-> ( y e. On /\ [. y / x ]. ph ) )
5 4 simprbi 
 |-  ( y e. { x e. On | ph } -> [. y / x ]. ph )
6 5 ralimi 
 |-  ( A. y e. z y e. { x e. On | ph } -> A. y e. z [. y / x ]. ph )
7 2 6 sylbi 
 |-  ( z C_ { x e. On | ph } -> A. y e. z [. y / x ]. ph )
8 nfcv 
 |-  F/_ x z
9 nfsbc1v 
 |-  F/ x [. y / x ]. ph
10 8 9 nfralw 
 |-  F/ x A. y e. z [. y / x ]. ph
11 nfsbc1v 
 |-  F/ x [. z / x ]. ph
12 10 11 nfim 
 |-  F/ x ( A. y e. z [. y / x ]. ph -> [. z / x ]. ph )
13 raleq 
 |-  ( x = z -> ( A. y e. x [. y / x ]. ph <-> A. y e. z [. y / x ]. ph ) )
14 sbceq1a 
 |-  ( x = z -> ( ph <-> [. z / x ]. ph ) )
15 13 14 imbi12d 
 |-  ( x = z -> ( ( A. y e. x [. y / x ]. ph -> ph ) <-> ( A. y e. z [. y / x ]. ph -> [. z / x ]. ph ) ) )
16 12 15 rspc 
 |-  ( z e. On -> ( A. x e. On ( A. y e. x [. y / x ]. ph -> ph ) -> ( A. y e. z [. y / x ]. ph -> [. z / x ]. ph ) ) )
17 16 impcom 
 |-  ( ( A. x e. On ( A. y e. x [. y / x ]. ph -> ph ) /\ z e. On ) -> ( A. y e. z [. y / x ]. ph -> [. z / x ]. ph ) )
18 7 17 syl5 
 |-  ( ( A. x e. On ( A. y e. x [. y / x ]. ph -> ph ) /\ z e. On ) -> ( z C_ { x e. On | ph } -> [. z / x ]. ph ) )
19 simpr 
 |-  ( ( A. x e. On ( A. y e. x [. y / x ]. ph -> ph ) /\ z e. On ) -> z e. On )
20 18 19 jctild 
 |-  ( ( A. x e. On ( A. y e. x [. y / x ]. ph -> ph ) /\ z e. On ) -> ( z C_ { x e. On | ph } -> ( z e. On /\ [. z / x ]. ph ) ) )
21 3 elrabsf 
 |-  ( z e. { x e. On | ph } <-> ( z e. On /\ [. z / x ]. ph ) )
22 20 21 syl6ibr 
 |-  ( ( A. x e. On ( A. y e. x [. y / x ]. ph -> ph ) /\ z e. On ) -> ( z C_ { x e. On | ph } -> z e. { x e. On | ph } ) )
23 22 ralrimiva 
 |-  ( A. x e. On ( A. y e. x [. y / x ]. ph -> ph ) -> A. z e. On ( z C_ { x e. On | ph } -> z e. { x e. On | ph } ) )
24 tfi 
 |-  ( ( { x e. On | ph } C_ On /\ A. z e. On ( z C_ { x e. On | ph } -> z e. { x e. On | ph } ) ) -> { x e. On | ph } = On )
25 1 23 24 sylancr 
 |-  ( A. x e. On ( A. y e. x [. y / x ]. ph -> ph ) -> { x e. On | ph } = On )
26 25 eqcomd 
 |-  ( A. x e. On ( A. y e. x [. y / x ]. ph -> ph ) -> On = { x e. On | ph } )
27 rabid2 
 |-  ( On = { x e. On | ph } <-> A. x e. On ph )
28 26 27 sylib 
 |-  ( A. x e. On ( A. y e. x [. y / x ]. ph -> ph ) -> A. x e. On ph )