Metamath Proof Explorer

Theorem bnj1523

Description: Technical lemma for bnj1522 . 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 bnj1523.1 
|- B = { d | ( d C_ A /\ A. x e. d _pred ( x , A , R ) C_ d ) }
bnj1523.2 
|- Y = <. x , ( f |` _pred ( x , A , R ) ) >.
bnj1523.3 
|- C = { f | E. d e. B ( f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) }
bnj1523.4 
|- F = U. C
bnj1523.5 
|- ( ph <-> ( R _FrSe A /\ H Fn A /\ A. x e. A ( H ` x ) = ( G ` <. x , ( H |` _pred ( x , A , R ) ) >. ) ) )
bnj1523.6 
|- ( ps <-> ( ph /\ F =/= H ) )
bnj1523.7 
|- ( ch <-> ( ps /\ x e. A /\ ( F ` x ) =/= ( H ` x ) ) )
bnj1523.8 
|- D = { x e. A | ( F ` x ) =/= ( H ` x ) }
bnj1523.9 
|- ( th <-> ( ch /\ y e. D /\ A. z e. D -. z R y ) )
Assertion bnj1523 
|- ( ( R _FrSe A /\ H Fn A /\ A. x e. A ( H ` x ) = ( G ` <. x , ( H |` _pred ( x , A , R ) ) >. ) ) -> F = H )

Proof

Step Hyp Ref Expression
1 bnj1523.1 
 |-  B = { d | ( d C_ A /\ A. x e. d _pred ( x , A , R ) C_ d ) }
2 bnj1523.2 
 |-  Y = <. x , ( f |` _pred ( x , A , R ) ) >.
3 bnj1523.3 
 |-  C = { f | E. d e. B ( f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) }
4 bnj1523.4 
 |-  F = U. C
5 bnj1523.5 
 |-  ( ph <-> ( R _FrSe A /\ H Fn A /\ A. x e. A ( H ` x ) = ( G ` <. x , ( H |` _pred ( x , A , R ) ) >. ) ) )
6 bnj1523.6 
 |-  ( ps <-> ( ph /\ F =/= H ) )
7 bnj1523.7 
 |-  ( ch <-> ( ps /\ x e. A /\ ( F ` x ) =/= ( H ` x ) ) )
8 bnj1523.8 
 |-  D = { x e. A | ( F ` x ) =/= ( H ` x ) }
9 bnj1523.9 
 |-  ( th <-> ( ch /\ y e. D /\ A. z e. D -. z R y ) )
10 1 2 3 4 bnj60 
 |-  ( R _FrSe A -> F Fn A )
11 5 10 bnj835 
 |-  ( ph -> F Fn A )
12 6 11 bnj832 
 |-  ( ps -> F Fn A )
13 7 12 bnj835 
 |-  ( ch -> F Fn A )
14 9 13 bnj835 
 |-  ( th -> F Fn A )
15 5 simp2bi 
 |-  ( ph -> H Fn A )
16 6 15 bnj832 
 |-  ( ps -> H Fn A )
17 7 16 bnj835 
 |-  ( ch -> H Fn A )
18 9 17 bnj835 
 |-  ( th -> H Fn A )
19 bnj213 
 |-  _pred ( y , A , R ) C_ A
20 19 a1i 
 |-  ( th -> _pred ( y , A , R ) C_ A )
21 9 simp3bi 
 |-  ( th -> A. z e. D -. z R y )
22 21 bnj1211 
 |-  ( th -> A. z ( z e. D -> -. z R y ) )
23 con2b 
 |-  ( ( z e. D -> -. z R y ) <-> ( z R y -> -. z e. D ) )
24 23 albii 
 |-  ( A. z ( z e. D -> -. z R y ) <-> A. z ( z R y -> -. z e. D ) )
25 22 24 sylib 
 |-  ( th -> A. z ( z R y -> -. z e. D ) )
26 bnj1418 
 |-  ( z e. _pred ( y , A , R ) -> z R y )
27 26 imim1i 
 |-  ( ( z R y -> -. z e. D ) -> ( z e. _pred ( y , A , R ) -> -. z e. D ) )
28 27 alimi 
 |-  ( A. z ( z R y -> -. z e. D ) -> A. z ( z e. _pred ( y , A , R ) -> -. z e. D ) )
29 25 28 syl 
 |-  ( th -> A. z ( z e. _pred ( y , A , R ) -> -. z e. D ) )
30 29 bnj1142 
 |-  ( th -> A. z e. _pred ( y , A , R ) -. z e. D )
31 1 bnj1309 
 |-  ( w e. B -> A. x w e. B )
32 3 31 bnj1307 
 |-  ( w e. C -> A. x w e. C )
33 32 nfcii 
 |-  F/_ x C
34 33 nfuni 
 |-  F/_ x U. C
35 4 34 nfcxfr 
 |-  F/_ x F
36 35 nfcrii 
 |-  ( w e. F -> A. x w e. F )
37 8 36 bnj1534 
 |-  D = { z e. A | ( F ` z ) =/= ( H ` z ) }
38 30 19 37 bnj1533 
 |-  ( th -> A. z e. _pred ( y , A , R ) ( F ` z ) = ( H ` z ) )
39 14 18 20 38 bnj1536 
 |-  ( th -> ( F |` _pred ( y , A , R ) ) = ( H |` _pred ( y , A , R ) ) )
40 39 opeq2d 
 |-  ( th -> <. y , ( F |` _pred ( y , A , R ) ) >. = <. y , ( H |` _pred ( y , A , R ) ) >. )
41 40 fveq2d 
 |-  ( th -> ( G ` <. y , ( F |` _pred ( y , A , R ) ) >. ) = ( G ` <. y , ( H |` _pred ( y , A , R ) ) >. ) )
42 1 2 3 4 bnj1500 
 |-  ( R _FrSe A -> A. x e. A ( F ` x ) = ( G ` <. x , ( F |` _pred ( x , A , R ) ) >. ) )
43 5 42 bnj835 
 |-  ( ph -> A. x e. A ( F ` x ) = ( G ` <. x , ( F |` _pred ( x , A , R ) ) >. ) )
44 6 43 bnj832 
 |-  ( ps -> A. x e. A ( F ` x ) = ( G ` <. x , ( F |` _pred ( x , A , R ) ) >. ) )
45 7 44 bnj835 
 |-  ( ch -> A. x e. A ( F ` x ) = ( G ` <. x , ( F |` _pred ( x , A , R ) ) >. ) )
46 45 36 bnj1529 
 |-  ( ch -> A. y e. A ( F ` y ) = ( G ` <. y , ( F |` _pred ( y , A , R ) ) >. ) )
47 9 46 bnj835 
 |-  ( th -> A. y e. A ( F ` y ) = ( G ` <. y , ( F |` _pred ( y , A , R ) ) >. ) )
48 8 ssrab3 
 |-  D C_ A
49 9 simp2bi 
 |-  ( th -> y e. D )
50 48 49 bnj1213 
 |-  ( th -> y e. A )
51 47 50 bnj1294 
 |-  ( th -> ( F ` y ) = ( G ` <. y , ( F |` _pred ( y , A , R ) ) >. ) )
52 5 simp3bi 
 |-  ( ph -> A. x e. A ( H ` x ) = ( G ` <. x , ( H |` _pred ( x , A , R ) ) >. ) )
53 6 52 bnj832 
 |-  ( ps -> A. x e. A ( H ` x ) = ( G ` <. x , ( H |` _pred ( x , A , R ) ) >. ) )
54 7 53 bnj835 
 |-  ( ch -> A. x e. A ( H ` x ) = ( G ` <. x , ( H |` _pred ( x , A , R ) ) >. ) )
55 ax-5 
 |-  ( v e. H -> A. x v e. H )
56 54 55 bnj1529 
 |-  ( ch -> A. y e. A ( H ` y ) = ( G ` <. y , ( H |` _pred ( y , A , R ) ) >. ) )
57 9 56 bnj835 
 |-  ( th -> A. y e. A ( H ` y ) = ( G ` <. y , ( H |` _pred ( y , A , R ) ) >. ) )
58 57 50 bnj1294 
 |-  ( th -> ( H ` y ) = ( G ` <. y , ( H |` _pred ( y , A , R ) ) >. ) )
59 41 51 58 3eqtr4d 
 |-  ( th -> ( F ` y ) = ( H ` y ) )
60 8 36 bnj1534 
 |-  D = { y e. A | ( F ` y ) =/= ( H ` y ) }
61 60 bnj1538 
 |-  ( y e. D -> ( F ` y ) =/= ( H ` y ) )
62 9 61 bnj836 
 |-  ( th -> ( F ` y ) =/= ( H ` y ) )
63 62 neneqd 
 |-  ( th -> -. ( F ` y ) = ( H ` y ) )
64 59 63 pm2.65i 
 |-  -. th
65 64 nex 
 |-  -. E. y th
66 5 simp1bi 
 |-  ( ph -> R _FrSe A )
67 6 66 bnj832 
 |-  ( ps -> R _FrSe A )
68 7 67 bnj835 
 |-  ( ch -> R _FrSe A )
69 48 a1i 
 |-  ( ch -> D C_ A )
70 7 simp2bi 
 |-  ( ch -> x e. A )
71 7 simp3bi 
 |-  ( ch -> ( F ` x ) =/= ( H ` x ) )
72 8 rabeq2i 
 |-  ( x e. D <-> ( x e. A /\ ( F ` x ) =/= ( H ` x ) ) )
73 70 71 72 sylanbrc 
 |-  ( ch -> x e. D )
74 73 ne0d 
 |-  ( ch -> D =/= (/) )
75 bnj69 
 |-  ( ( R _FrSe A /\ D C_ A /\ D =/= (/) ) -> E. y e. D A. z e. D -. z R y )
76 68 69 74 75 syl3anc 
 |-  ( ch -> E. y e. D A. z e. D -. z R y )
77 76 9 bnj1209 
 |-  ( ch -> E. y th )
78 65 77 mto 
 |-  -. ch
79 78 nex 
 |-  -. E. x ch
80 6 simprbi 
 |-  ( ps -> F =/= H )
81 12 16 80 36 bnj1542 
 |-  ( ps -> E. x e. A ( F ` x ) =/= ( H ` x ) )
82 1 2 3 4 5 6 bnj1525 
 |-  ( ps -> A. x ps )
83 81 7 82 bnj1521 
 |-  ( ps -> E. x ch )
84 79 83 mto 
 |-  -. ps
85 6 84 bnj1541 
 |-  ( ph -> F = H )
86 5 85 sylbir 
 |-  ( ( R _FrSe A /\ H Fn A /\ A. x e. A ( H ` x ) = ( G ` <. x , ( H |` _pred ( x , A , R ) ) >. ) ) -> F = H )