Metamath Proof Explorer

Theorem bnj1442

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 bnj1442.1 
|- B = { d | ( d C_ A /\ A. x e. d _pred ( x , A , R ) C_ d ) }
bnj1442.2 
|- Y = <. x , ( f |` _pred ( x , A , R ) ) >.
bnj1442.3 
|- C = { f | E. d e. B ( f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) }
bnj1442.4 
|- ( ta <-> ( f e. C /\ dom f = ( { x } u. _trCl ( x , A , R ) ) ) )
bnj1442.5 
|- D = { x e. A | -. E. f ta }
bnj1442.6 
|- ( ps <-> ( R _FrSe A /\ D =/= (/) ) )
bnj1442.7 
|- ( ch <-> ( ps /\ x e. D /\ A. y e. D -. y R x ) )
bnj1442.8 
|- ( ta' <-> [. y / x ]. ta )
bnj1442.9 
|- H = { f | E. y e. _pred ( x , A , R ) ta' }
bnj1442.10 
|- P = U. H
bnj1442.11 
|- Z = <. x , ( P |` _pred ( x , A , R ) ) >.
bnj1442.12 
|- Q = ( P u. { <. x , ( G ` Z ) >. } )
bnj1442.13 
|- W = <. z , ( Q |` _pred ( z , A , R ) ) >.
bnj1442.14 
|- E = ( { x } u. _trCl ( x , A , R ) )
bnj1442.15 
|- ( ch -> P Fn _trCl ( x , A , R ) )
bnj1442.16 
|- ( ch -> Q Fn ( { x } u. _trCl ( x , A , R ) ) )
bnj1442.17 
|- ( th <-> ( ch /\ z e. E ) )
bnj1442.18 
|- ( et <-> ( th /\ z e. { x } ) )
Assertion bnj1442 
|- ( et -> ( Q ` z ) = ( G ` W ) )

Proof

Step Hyp Ref Expression
1 bnj1442.1 
 |-  B = { d | ( d C_ A /\ A. x e. d _pred ( x , A , R ) C_ d ) }
2 bnj1442.2 
 |-  Y = <. x , ( f |` _pred ( x , A , R ) ) >.
3 bnj1442.3 
 |-  C = { f | E. d e. B ( f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) }
4 bnj1442.4 
 |-  ( ta <-> ( f e. C /\ dom f = ( { x } u. _trCl ( x , A , R ) ) ) )
5 bnj1442.5 
 |-  D = { x e. A | -. E. f ta }
6 bnj1442.6 
 |-  ( ps <-> ( R _FrSe A /\ D =/= (/) ) )
7 bnj1442.7 
 |-  ( ch <-> ( ps /\ x e. D /\ A. y e. D -. y R x ) )
8 bnj1442.8 
 |-  ( ta' <-> [. y / x ]. ta )
9 bnj1442.9 
 |-  H = { f | E. y e. _pred ( x , A , R ) ta' }
10 bnj1442.10 
 |-  P = U. H
11 bnj1442.11 
 |-  Z = <. x , ( P |` _pred ( x , A , R ) ) >.
12 bnj1442.12 
 |-  Q = ( P u. { <. x , ( G ` Z ) >. } )
13 bnj1442.13 
 |-  W = <. z , ( Q |` _pred ( z , A , R ) ) >.
14 bnj1442.14 
 |-  E = ( { x } u. _trCl ( x , A , R ) )
15 bnj1442.15 
 |-  ( ch -> P Fn _trCl ( x , A , R ) )
16 bnj1442.16 
 |-  ( ch -> Q Fn ( { x } u. _trCl ( x , A , R ) ) )
17 bnj1442.17 
 |-  ( th <-> ( ch /\ z e. E ) )
18 bnj1442.18 
 |-  ( et <-> ( th /\ z e. { x } ) )
19 16 bnj930 
 |-  ( ch -> Fun Q )
20 opex 
 |-  <. x , ( G ` Z ) >. e. _V
21 20 snid 
 |-  <. x , ( G ` Z ) >. e. { <. x , ( G ` Z ) >. }
22 elun2 
 |-  ( <. x , ( G ` Z ) >. e. { <. x , ( G ` Z ) >. } -> <. x , ( G ` Z ) >. e. ( P u. { <. x , ( G ` Z ) >. } ) )
23 21 22 ax-mp 
 |-  <. x , ( G ` Z ) >. e. ( P u. { <. x , ( G ` Z ) >. } )
24 23 12 eleqtrri 
 |-  <. x , ( G ` Z ) >. e. Q
25 funopfv 
 |-  ( Fun Q -> ( <. x , ( G ` Z ) >. e. Q -> ( Q ` x ) = ( G ` Z ) ) )
26 19 24 25 mpisyl 
 |-  ( ch -> ( Q ` x ) = ( G ` Z ) )
27 17 26 bnj832 
 |-  ( th -> ( Q ` x ) = ( G ` Z ) )
28 18 27 bnj832 
 |-  ( et -> ( Q ` x ) = ( G ` Z ) )
29 elsni 
 |-  ( z e. { x } -> z = x )
30 18 29 simplbiim 
 |-  ( et -> z = x )
31 30 fveq2d 
 |-  ( et -> ( Q ` z ) = ( Q ` x ) )
32 bnj602 
 |-  ( z = x -> _pred ( z , A , R ) = _pred ( x , A , R ) )
33 32 reseq2d 
 |-  ( z = x -> ( Q |` _pred ( z , A , R ) ) = ( Q |` _pred ( x , A , R ) ) )
34 30 33 syl 
 |-  ( et -> ( Q |` _pred ( z , A , R ) ) = ( Q |` _pred ( x , A , R ) ) )
35 12 bnj931 
 |-  P C_ Q
36 35 a1i 
 |-  ( ch -> P C_ Q )
37 6 simplbi 
 |-  ( ps -> R _FrSe A )
38 7 37 bnj835 
 |-  ( ch -> R _FrSe A )
39 5 7 bnj1212 
 |-  ( ch -> x e. A )
40 bnj906 
 |-  ( ( R _FrSe A /\ x e. A ) -> _pred ( x , A , R ) C_ _trCl ( x , A , R ) )
41 38 39 40 syl2anc 
 |-  ( ch -> _pred ( x , A , R ) C_ _trCl ( x , A , R ) )
42 15 fndmd 
 |-  ( ch -> dom P = _trCl ( x , A , R ) )
43 41 42 sseqtrrd 
 |-  ( ch -> _pred ( x , A , R ) C_ dom P )
44 19 36 43 bnj1503 
 |-  ( ch -> ( Q |` _pred ( x , A , R ) ) = ( P |` _pred ( x , A , R ) ) )
45 17 44 bnj832 
 |-  ( th -> ( Q |` _pred ( x , A , R ) ) = ( P |` _pred ( x , A , R ) ) )
46 18 45 bnj832 
 |-  ( et -> ( Q |` _pred ( x , A , R ) ) = ( P |` _pred ( x , A , R ) ) )
47 34 46 eqtrd 
 |-  ( et -> ( Q |` _pred ( z , A , R ) ) = ( P |` _pred ( x , A , R ) ) )
48 30 47 opeq12d 
 |-  ( et -> <. z , ( Q |` _pred ( z , A , R ) ) >. = <. x , ( P |` _pred ( x , A , R ) ) >. )
49 48 13 11 3eqtr4g 
 |-  ( et -> W = Z )
50 49 fveq2d 
 |-  ( et -> ( G ` W ) = ( G ` Z ) )
51 28 31 50 3eqtr4d 
 |-  ( et -> ( Q ` z ) = ( G ` W ) )