Metamath Proof Explorer


Theorem bnj1321

Description: Technical lemma for bnj60 . This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

Ref Expression
Hypotheses bnj1321.1
|- B = { d | ( d C_ A /\ A. x e. d _pred ( x , A , R ) C_ d ) }
bnj1321.2
|- Y = <. x , ( f |` _pred ( x , A , R ) ) >.
bnj1321.3
|- C = { f | E. d e. B ( f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) }
bnj1321.4
|- ( ta <-> ( f e. C /\ dom f = ( { x } u. _trCl ( x , A , R ) ) ) )
Assertion bnj1321
|- ( ( R _FrSe A /\ E. f ta ) -> E! f ta )

Proof

Step Hyp Ref Expression
1 bnj1321.1
 |-  B = { d | ( d C_ A /\ A. x e. d _pred ( x , A , R ) C_ d ) }
2 bnj1321.2
 |-  Y = <. x , ( f |` _pred ( x , A , R ) ) >.
3 bnj1321.3
 |-  C = { f | E. d e. B ( f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) }
4 bnj1321.4
 |-  ( ta <-> ( f e. C /\ dom f = ( { x } u. _trCl ( x , A , R ) ) ) )
5 simpr
 |-  ( ( R _FrSe A /\ E. f ta ) -> E. f ta )
6 simp1
 |-  ( ( R _FrSe A /\ ta /\ [ g / f ] ta ) -> R _FrSe A )
7 4 simplbi
 |-  ( ta -> f e. C )
8 7 3ad2ant2
 |-  ( ( R _FrSe A /\ ta /\ [ g / f ] ta ) -> f e. C )
9 nfab1
 |-  F/_ f { f | E. d e. B ( f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) }
10 3 9 nfcxfr
 |-  F/_ f C
11 10 nfcri
 |-  F/ f g e. C
12 nfv
 |-  F/ f dom g = ( { x } u. _trCl ( x , A , R ) )
13 11 12 nfan
 |-  F/ f ( g e. C /\ dom g = ( { x } u. _trCl ( x , A , R ) ) )
14 eleq1w
 |-  ( f = g -> ( f e. C <-> g e. C ) )
15 dmeq
 |-  ( f = g -> dom f = dom g )
16 15 eqeq1d
 |-  ( f = g -> ( dom f = ( { x } u. _trCl ( x , A , R ) ) <-> dom g = ( { x } u. _trCl ( x , A , R ) ) ) )
17 14 16 anbi12d
 |-  ( f = g -> ( ( f e. C /\ dom f = ( { x } u. _trCl ( x , A , R ) ) ) <-> ( g e. C /\ dom g = ( { x } u. _trCl ( x , A , R ) ) ) ) )
18 4 17 syl5bb
 |-  ( f = g -> ( ta <-> ( g e. C /\ dom g = ( { x } u. _trCl ( x , A , R ) ) ) ) )
19 13 18 sbiev
 |-  ( [ g / f ] ta <-> ( g e. C /\ dom g = ( { x } u. _trCl ( x , A , R ) ) ) )
20 19 simplbi
 |-  ( [ g / f ] ta -> g e. C )
21 20 3ad2ant3
 |-  ( ( R _FrSe A /\ ta /\ [ g / f ] ta ) -> g e. C )
22 eqid
 |-  ( dom f i^i dom g ) = ( dom f i^i dom g )
23 1 2 3 22 bnj1326
 |-  ( ( R _FrSe A /\ f e. C /\ g e. C ) -> ( f |` ( dom f i^i dom g ) ) = ( g |` ( dom f i^i dom g ) ) )
24 6 8 21 23 syl3anc
 |-  ( ( R _FrSe A /\ ta /\ [ g / f ] ta ) -> ( f |` ( dom f i^i dom g ) ) = ( g |` ( dom f i^i dom g ) ) )
25 4 simprbi
 |-  ( ta -> dom f = ( { x } u. _trCl ( x , A , R ) ) )
26 25 3ad2ant2
 |-  ( ( R _FrSe A /\ ta /\ [ g / f ] ta ) -> dom f = ( { x } u. _trCl ( x , A , R ) ) )
27 19 simprbi
 |-  ( [ g / f ] ta -> dom g = ( { x } u. _trCl ( x , A , R ) ) )
28 27 3ad2ant3
 |-  ( ( R _FrSe A /\ ta /\ [ g / f ] ta ) -> dom g = ( { x } u. _trCl ( x , A , R ) ) )
29 26 28 eqtr4d
 |-  ( ( R _FrSe A /\ ta /\ [ g / f ] ta ) -> dom f = dom g )
30 bnj1322
 |-  ( dom f = dom g -> ( dom f i^i dom g ) = dom f )
31 30 reseq2d
 |-  ( dom f = dom g -> ( f |` ( dom f i^i dom g ) ) = ( f |` dom f ) )
32 29 31 syl
 |-  ( ( R _FrSe A /\ ta /\ [ g / f ] ta ) -> ( f |` ( dom f i^i dom g ) ) = ( f |` dom f ) )
33 releq
 |-  ( z = f -> ( Rel z <-> Rel f ) )
34 1 2 3 bnj66
 |-  ( z e. C -> Rel z )
35 33 34 vtoclga
 |-  ( f e. C -> Rel f )
36 resdm
 |-  ( Rel f -> ( f |` dom f ) = f )
37 8 35 36 3syl
 |-  ( ( R _FrSe A /\ ta /\ [ g / f ] ta ) -> ( f |` dom f ) = f )
38 32 37 eqtrd
 |-  ( ( R _FrSe A /\ ta /\ [ g / f ] ta ) -> ( f |` ( dom f i^i dom g ) ) = f )
39 eqeq2
 |-  ( dom f = dom g -> ( ( dom f i^i dom g ) = dom f <-> ( dom f i^i dom g ) = dom g ) )
40 30 39 mpbid
 |-  ( dom f = dom g -> ( dom f i^i dom g ) = dom g )
41 40 reseq2d
 |-  ( dom f = dom g -> ( g |` ( dom f i^i dom g ) ) = ( g |` dom g ) )
42 29 41 syl
 |-  ( ( R _FrSe A /\ ta /\ [ g / f ] ta ) -> ( g |` ( dom f i^i dom g ) ) = ( g |` dom g ) )
43 1 2 3 bnj66
 |-  ( g e. C -> Rel g )
44 resdm
 |-  ( Rel g -> ( g |` dom g ) = g )
45 21 43 44 3syl
 |-  ( ( R _FrSe A /\ ta /\ [ g / f ] ta ) -> ( g |` dom g ) = g )
46 42 45 eqtrd
 |-  ( ( R _FrSe A /\ ta /\ [ g / f ] ta ) -> ( g |` ( dom f i^i dom g ) ) = g )
47 24 38 46 3eqtr3d
 |-  ( ( R _FrSe A /\ ta /\ [ g / f ] ta ) -> f = g )
48 47 3expib
 |-  ( R _FrSe A -> ( ( ta /\ [ g / f ] ta ) -> f = g ) )
49 48 alrimivv
 |-  ( R _FrSe A -> A. f A. g ( ( ta /\ [ g / f ] ta ) -> f = g ) )
50 49 adantr
 |-  ( ( R _FrSe A /\ E. f ta ) -> A. f A. g ( ( ta /\ [ g / f ] ta ) -> f = g ) )
51 nfv
 |-  F/ g ta
52 51 eu2
 |-  ( E! f ta <-> ( E. f ta /\ A. f A. g ( ( ta /\ [ g / f ] ta ) -> f = g ) ) )
53 5 50 52 sylanbrc
 |-  ( ( R _FrSe A /\ E. f ta ) -> E! f ta )