Metamath Proof Explorer

Theorem bnj1450

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

Proof

Step Hyp Ref Expression
1 bnj1450.1 
 |-  B = { d | ( d C_ A /\ A. x e. d _pred ( x , A , R ) C_ d ) }
2 bnj1450.2 
 |-  Y = <. x , ( f |` _pred ( x , A , R ) ) >.
3 bnj1450.3 
 |-  C = { f | E. d e. B ( f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) }
4 bnj1450.4 
 |-  ( ta <-> ( f e. C /\ dom f = ( { x } u. _trCl ( x , A , R ) ) ) )
5 bnj1450.5 
 |-  D = { x e. A | -. E. f ta }
6 bnj1450.6 
 |-  ( ps <-> ( R _FrSe A /\ D =/= (/) ) )
7 bnj1450.7 
 |-  ( ch <-> ( ps /\ x e. D /\ A. y e. D -. y R x ) )
8 bnj1450.8 
 |-  ( ta' <-> [. y / x ]. ta )
9 bnj1450.9 
 |-  H = { f | E. y e. _pred ( x , A , R ) ta' }
10 bnj1450.10 
 |-  P = U. H
11 bnj1450.11 
 |-  Z = <. x , ( P |` _pred ( x , A , R ) ) >.
12 bnj1450.12 
 |-  Q = ( P u. { <. x , ( G ` Z ) >. } )
13 bnj1450.13 
 |-  W = <. z , ( Q |` _pred ( z , A , R ) ) >.
14 bnj1450.14 
 |-  E = ( { x } u. _trCl ( x , A , R ) )
15 bnj1450.15 
 |-  ( ch -> P Fn _trCl ( x , A , R ) )
16 bnj1450.16 
 |-  ( ch -> Q Fn ( { x } u. _trCl ( x , A , R ) ) )
17 bnj1450.17 
 |-  ( th <-> ( ch /\ z e. E ) )
18 bnj1450.18 
 |-  ( et <-> ( th /\ z e. { x } ) )
19 bnj1450.19 
 |-  ( ze <-> ( th /\ z e. _trCl ( x , A , R ) ) )
20 bnj1450.20 
 |-  ( rh <-> ( ze /\ f e. H /\ z e. dom f ) )
21 bnj1450.21 
 |-  ( si <-> ( rh /\ y e. _pred ( x , A , R ) /\ f e. C /\ dom f = ( { y } u. _trCl ( y , A , R ) ) ) )
22 bnj1450.22 
 |-  ( ph <-> ( si /\ d e. B /\ f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) )
23 bnj1450.23 
 |-  X = <. z , ( f |` _pred ( z , A , R ) ) >.
24 19 simprbi 
 |-  ( ze -> z e. _trCl ( x , A , R ) )
25 15 fndmd 
 |-  ( ch -> dom P = _trCl ( x , A , R ) )
26 17 25 bnj832 
 |-  ( th -> dom P = _trCl ( x , A , R ) )
27 19 26 bnj832 
 |-  ( ze -> dom P = _trCl ( x , A , R ) )
28 24 27 eleqtrrd 
 |-  ( ze -> z e. dom P )
29 10 dmeqi 
 |-  dom P = dom U. H
30 28 29 eleqtrdi 
 |-  ( ze -> z e. dom U. H )
31 9 bnj1317 
 |-  ( w e. H -> A. f w e. H )
32 31 bnj1400 
 |-  dom U. H = U_ f e. H dom f
33 30 32 eleqtrdi 
 |-  ( ze -> z e. U_ f e. H dom f )
34 33 bnj1405 
 |-  ( ze -> E. f e. H z e. dom f )
35 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 bnj1449 
 |-  ( ze -> A. f ze )
36 34 20 35 bnj1521 
 |-  ( ze -> E. f rh )
37 9 bnj1436 
 |-  ( f e. H -> E. y e. _pred ( x , A , R ) ta' )
38 20 37 bnj836 
 |-  ( rh -> E. y e. _pred ( x , A , R ) ta' )
39 1 2 3 4 8 bnj1373 
 |-  ( ta' <-> ( f e. C /\ dom f = ( { y } u. _trCl ( y , A , R ) ) ) )
40 39 rexbii 
 |-  ( E. y e. _pred ( x , A , R ) ta' <-> E. y e. _pred ( x , A , R ) ( f e. C /\ dom f = ( { y } u. _trCl ( y , A , R ) ) ) )
41 38 40 sylib 
 |-  ( rh -> E. y e. _pred ( x , A , R ) ( f e. C /\ dom f = ( { y } u. _trCl ( y , A , R ) ) ) )
42 41 bnj1196 
 |-  ( rh -> E. y ( y e. _pred ( x , A , R ) /\ ( f e. C /\ dom f = ( { y } u. _trCl ( y , A , R ) ) ) ) )
43 3anass 
 |-  ( ( y e. _pred ( x , A , R ) /\ f e. C /\ dom f = ( { y } u. _trCl ( y , A , R ) ) ) <-> ( y e. _pred ( x , A , R ) /\ ( f e. C /\ dom f = ( { y } u. _trCl ( y , A , R ) ) ) ) )
44 42 43 bnj1198 
 |-  ( rh -> E. y ( y e. _pred ( x , A , R ) /\ f e. C /\ dom f = ( { y } u. _trCl ( y , A , R ) ) ) )
45 bnj252 
 |-  ( ( rh /\ y e. _pred ( x , A , R ) /\ f e. C /\ dom f = ( { y } u. _trCl ( y , A , R ) ) ) <-> ( rh /\ ( y e. _pred ( x , A , R ) /\ f e. C /\ dom f = ( { y } u. _trCl ( y , A , R ) ) ) ) )
46 21 45 bitri 
 |-  ( si <-> ( rh /\ ( y e. _pred ( x , A , R ) /\ f e. C /\ dom f = ( { y } u. _trCl ( y , A , R ) ) ) ) )
47 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 bnj1444 
 |-  ( rh -> A. y rh )
48 44 46 47 bnj1340 
 |-  ( rh -> E. y si )
49 3 bnj1436 
 |-  ( f e. C -> E. d e. B ( f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) )
50 21 49 bnj771 
 |-  ( si -> E. d e. B ( f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) )
51 50 bnj1196 
 |-  ( si -> E. d ( d e. B /\ ( f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) ) )
52 3anass 
 |-  ( ( d e. B /\ f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) <-> ( d e. B /\ ( f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) ) )
53 51 52 bnj1198 
 |-  ( si -> E. d ( d e. B /\ f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) )
54 bnj252 
 |-  ( ( si /\ d e. B /\ f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) <-> ( si /\ ( d e. B /\ f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) ) )
55 22 54 bitri 
 |-  ( ph <-> ( si /\ ( d e. B /\ f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) ) )
56 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 bnj1445 
 |-  ( si -> A. d si )
57 53 55 56 bnj1340 
 |-  ( si -> E. d ph )
58 fveq2 
 |-  ( x = z -> ( f ` x ) = ( f ` z ) )
59 id 
 |-  ( x = z -> x = z )
60 bnj602 
 |-  ( x = z -> _pred ( x , A , R ) = _pred ( z , A , R ) )
61 60 reseq2d 
 |-  ( x = z -> ( f |` _pred ( x , A , R ) ) = ( f |` _pred ( z , A , R ) ) )
62 59 61 opeq12d 
 |-  ( x = z -> <. x , ( f |` _pred ( x , A , R ) ) >. = <. z , ( f |` _pred ( z , A , R ) ) >. )
63 62 2 23 3eqtr4g 
 |-  ( x = z -> Y = X )
64 63 fveq2d 
 |-  ( x = z -> ( G ` Y ) = ( G ` X ) )
65 58 64 eqeq12d 
 |-  ( x = z -> ( ( f ` x ) = ( G ` Y ) <-> ( f ` z ) = ( G ` X ) ) )
66 22 bnj1254 
 |-  ( ph -> A. x e. d ( f ` x ) = ( G ` Y ) )
67 20 simp3bi 
 |-  ( rh -> z e. dom f )
68 21 67 bnj769 
 |-  ( si -> z e. dom f )
69 22 68 bnj769 
 |-  ( ph -> z e. dom f )
70 fndm 
 |-  ( f Fn d -> dom f = d )
71 22 70 bnj771 
 |-  ( ph -> dom f = d )
72 69 71 eleqtrd 
 |-  ( ph -> z e. d )
73 65 66 72 rspcdva 
 |-  ( ph -> ( f ` z ) = ( G ` X ) )
74 16 bnj930 
 |-  ( ch -> Fun Q )
75 17 74 bnj832 
 |-  ( th -> Fun Q )
76 19 75 bnj832 
 |-  ( ze -> Fun Q )
77 20 76 bnj835 
 |-  ( rh -> Fun Q )
78 21 77 bnj769 
 |-  ( si -> Fun Q )
79 22 78 bnj769 
 |-  ( ph -> Fun Q )
80 20 simp2bi 
 |-  ( rh -> f e. H )
81 21 80 bnj769 
 |-  ( si -> f e. H )
82 22 81 bnj769 
 |-  ( ph -> f e. H )
83 elssuni 
 |-  ( f e. H -> f C_ U. H )
84 83 10 sseqtrrdi 
 |-  ( f e. H -> f C_ P )
85 ssun3 
 |-  ( f C_ P -> f C_ ( P u. { <. x , ( G ` Z ) >. } ) )
86 85 12 sseqtrrdi 
 |-  ( f C_ P -> f C_ Q )
87 82 84 86 3syl 
 |-  ( ph -> f C_ Q )
88 79 87 69 bnj1502 
 |-  ( ph -> ( Q ` z ) = ( f ` z ) )
89 60 sseq1d 
 |-  ( x = z -> ( _pred ( x , A , R ) C_ d <-> _pred ( z , A , R ) C_ d ) )
90 1 bnj1517 
 |-  ( d e. B -> A. x e. d _pred ( x , A , R ) C_ d )
91 22 90 bnj770 
 |-  ( ph -> A. x e. d _pred ( x , A , R ) C_ d )
92 89 91 72 rspcdva 
 |-  ( ph -> _pred ( z , A , R ) C_ d )
93 92 71 sseqtrrd 
 |-  ( ph -> _pred ( z , A , R ) C_ dom f )
94 79 87 93 bnj1503 
 |-  ( ph -> ( Q |` _pred ( z , A , R ) ) = ( f |` _pred ( z , A , R ) ) )
95 94 opeq2d 
 |-  ( ph -> <. z , ( Q |` _pred ( z , A , R ) ) >. = <. z , ( f |` _pred ( z , A , R ) ) >. )
96 95 13 23 3eqtr4g 
 |-  ( ph -> W = X )
97 96 fveq2d 
 |-  ( ph -> ( G ` W ) = ( G ` X ) )
98 73 88 97 3eqtr4d 
 |-  ( ph -> ( Q ` z ) = ( G ` W ) )
99 57 98 bnj593 
 |-  ( si -> E. d ( Q ` z ) = ( G ` W ) )
100 1 2 3 4 5 6 7 8 9 10 11 12 13 bnj1446 
 |-  ( ( Q ` z ) = ( G ` W ) -> A. d ( Q ` z ) = ( G ` W ) )
101 99 100 bnj1397 
 |-  ( si -> ( Q ` z ) = ( G ` W ) )
102 48 101 bnj593 
 |-  ( rh -> E. y ( Q ` z ) = ( G ` W ) )
103 1 2 3 4 5 6 7 8 9 10 11 12 13 bnj1447 
 |-  ( ( Q ` z ) = ( G ` W ) -> A. y ( Q ` z ) = ( G ` W ) )
104 102 103 bnj1397 
 |-  ( rh -> ( Q ` z ) = ( G ` W ) )
105 36 104 bnj593 
 |-  ( ze -> E. f ( Q ` z ) = ( G ` W ) )
106 1 2 3 4 5 6 7 8 9 10 11 12 13 bnj1448 
 |-  ( ( Q ` z ) = ( G ` W ) -> A. f ( Q ` z ) = ( G ` W ) )
107 105 106 bnj1397 
 |-  ( ze -> ( Q ` z ) = ( G ` W ) )