Metamath Proof Explorer


Theorem tfisg

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

Ref Expression
Assertion tfisg xOnyx[˙y/x]˙φφxOnφ

Proof

Step Hyp Ref Expression
1 ssrab2 xOn|φOn
2 dfss3 zxOn|φyzyxOn|φ
3 nfcv _xOn
4 3 elrabsf yxOn|φyOn[˙y/x]˙φ
5 4 simprbi yxOn|φ[˙y/x]˙φ
6 5 ralimi yzyxOn|φyz[˙y/x]˙φ
7 2 6 sylbi zxOn|φyz[˙y/x]˙φ
8 nfcv _xz
9 nfsbc1v x[˙y/x]˙φ
10 8 9 nfralw xyz[˙y/x]˙φ
11 nfsbc1v x[˙z/x]˙φ
12 10 11 nfim xyz[˙y/x]˙φ[˙z/x]˙φ
13 raleq x=zyx[˙y/x]˙φyz[˙y/x]˙φ
14 sbceq1a x=zφ[˙z/x]˙φ
15 13 14 imbi12d x=zyx[˙y/x]˙φφyz[˙y/x]˙φ[˙z/x]˙φ
16 12 15 rspc zOnxOnyx[˙y/x]˙φφyz[˙y/x]˙φ[˙z/x]˙φ
17 16 impcom xOnyx[˙y/x]˙φφzOnyz[˙y/x]˙φ[˙z/x]˙φ
18 7 17 syl5 xOnyx[˙y/x]˙φφzOnzxOn|φ[˙z/x]˙φ
19 simpr xOnyx[˙y/x]˙φφzOnzOn
20 18 19 jctild xOnyx[˙y/x]˙φφzOnzxOn|φzOn[˙z/x]˙φ
21 3 elrabsf zxOn|φzOn[˙z/x]˙φ
22 20 21 syl6ibr xOnyx[˙y/x]˙φφzOnzxOn|φzxOn|φ
23 22 ralrimiva xOnyx[˙y/x]˙φφzOnzxOn|φzxOn|φ
24 tfi xOn|φOnzOnzxOn|φzxOn|φxOn|φ=On
25 1 23 24 sylancr xOnyx[˙y/x]˙φφxOn|φ=On
26 25 eqcomd xOnyx[˙y/x]˙φφOn=xOn|φ
27 rabid2 On=xOn|φxOnφ
28 26 27 sylib xOnyx[˙y/x]˙φφxOnφ