Metamath Proof Explorer

Theorem bnj1452

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

Proof

Step Hyp Ref Expression
1 bnj1452.1 
 |-  B = { d | ( d C_ A /\ A. x e. d _pred ( x , A , R ) C_ d ) }
2 bnj1452.2 
 |-  Y = <. x , ( f |` _pred ( x , A , R ) ) >.
3 bnj1452.3 
 |-  C = { f | E. d e. B ( f Fn d /\ A. x e. d ( f ` x ) = ( G ` Y ) ) }
4 bnj1452.4 
 |-  ( ta <-> ( f e. C /\ dom f = ( { x } u. _trCl ( x , A , R ) ) ) )
5 bnj1452.5 
 |-  D = { x e. A | -. E. f ta }
6 bnj1452.6 
 |-  ( ps <-> ( R _FrSe A /\ D =/= (/) ) )
7 bnj1452.7 
 |-  ( ch <-> ( ps /\ x e. D /\ A. y e. D -. y R x ) )
8 bnj1452.8 
 |-  ( ta' <-> [. y / x ]. ta )
9 bnj1452.9 
 |-  H = { f | E. y e. _pred ( x , A , R ) ta' }
10 bnj1452.10 
 |-  P = U. H
11 bnj1452.11 
 |-  Z = <. x , ( P |` _pred ( x , A , R ) ) >.
12 bnj1452.12 
 |-  Q = ( P u. { <. x , ( G ` Z ) >. } )
13 bnj1452.13 
 |-  W = <. z , ( Q |` _pred ( z , A , R ) ) >.
14 bnj1452.14 
 |-  E = ( { x } u. _trCl ( x , A , R ) )
15 5 7 bnj1212 
 |-  ( ch -> x e. A )
16 15 snssd 
 |-  ( ch -> { x } C_ A )
17 bnj1147 
 |-  _trCl ( x , A , R ) C_ A
18 17 a1i 
 |-  ( ch -> _trCl ( x , A , R ) C_ A )
19 16 18 unssd 
 |-  ( ch -> ( { x } u. _trCl ( x , A , R ) ) C_ A )
20 14 19 eqsstrid 
 |-  ( ch -> E C_ A )
21 elsni 
 |-  ( z e. { x } -> z = x )
22 21 adantl 
 |-  ( ( ( ch /\ z e. E ) /\ z e. { x } ) -> z = x )
23 bnj602 
 |-  ( z = x -> _pred ( z , A , R ) = _pred ( x , A , R ) )
24 22 23 syl 
 |-  ( ( ( ch /\ z e. E ) /\ z e. { x } ) -> _pred ( z , A , R ) = _pred ( x , A , R ) )
25 6 simplbi 
 |-  ( ps -> R _FrSe A )
26 7 25 bnj835 
 |-  ( ch -> R _FrSe A )
27 bnj906 
 |-  ( ( R _FrSe A /\ x e. A ) -> _pred ( x , A , R ) C_ _trCl ( x , A , R ) )
28 26 15 27 syl2anc 
 |-  ( ch -> _pred ( x , A , R ) C_ _trCl ( x , A , R ) )
29 28 ad2antrr 
 |-  ( ( ( ch /\ z e. E ) /\ z e. { x } ) -> _pred ( x , A , R ) C_ _trCl ( x , A , R ) )
30 24 29 eqsstrd 
 |-  ( ( ( ch /\ z e. E ) /\ z e. { x } ) -> _pred ( z , A , R ) C_ _trCl ( x , A , R ) )
31 ssun4 
 |-  ( _pred ( z , A , R ) C_ _trCl ( x , A , R ) -> _pred ( z , A , R ) C_ ( { x } u. _trCl ( x , A , R ) ) )
32 31 14 sseqtrrdi 
 |-  ( _pred ( z , A , R ) C_ _trCl ( x , A , R ) -> _pred ( z , A , R ) C_ E )
33 30 32 syl 
 |-  ( ( ( ch /\ z e. E ) /\ z e. { x } ) -> _pred ( z , A , R ) C_ E )
34 26 ad2antrr 
 |-  ( ( ( ch /\ z e. E ) /\ z e. _trCl ( x , A , R ) ) -> R _FrSe A )
35 simpr 
 |-  ( ( ( ch /\ z e. E ) /\ z e. _trCl ( x , A , R ) ) -> z e. _trCl ( x , A , R ) )
36 17 35 bnj1213 
 |-  ( ( ( ch /\ z e. E ) /\ z e. _trCl ( x , A , R ) ) -> z e. A )
37 bnj906 
 |-  ( ( R _FrSe A /\ z e. A ) -> _pred ( z , A , R ) C_ _trCl ( z , A , R ) )
38 34 36 37 syl2anc 
 |-  ( ( ( ch /\ z e. E ) /\ z e. _trCl ( x , A , R ) ) -> _pred ( z , A , R ) C_ _trCl ( z , A , R ) )
39 15 ad2antrr 
 |-  ( ( ( ch /\ z e. E ) /\ z e. _trCl ( x , A , R ) ) -> x e. A )
40 bnj1125 
 |-  ( ( R _FrSe A /\ x e. A /\ z e. _trCl ( x , A , R ) ) -> _trCl ( z , A , R ) C_ _trCl ( x , A , R ) )
41 34 39 35 40 syl3anc 
 |-  ( ( ( ch /\ z e. E ) /\ z e. _trCl ( x , A , R ) ) -> _trCl ( z , A , R ) C_ _trCl ( x , A , R ) )
42 38 41 sstrd 
 |-  ( ( ( ch /\ z e. E ) /\ z e. _trCl ( x , A , R ) ) -> _pred ( z , A , R ) C_ _trCl ( x , A , R ) )
43 42 32 syl 
 |-  ( ( ( ch /\ z e. E ) /\ z e. _trCl ( x , A , R ) ) -> _pred ( z , A , R ) C_ E )
44 14 bnj1424 
 |-  ( z e. E -> ( z e. { x } \/ z e. _trCl ( x , A , R ) ) )
45 44 adantl 
 |-  ( ( ch /\ z e. E ) -> ( z e. { x } \/ z e. _trCl ( x , A , R ) ) )
46 33 43 45 mpjaodan 
 |-  ( ( ch /\ z e. E ) -> _pred ( z , A , R ) C_ E )
47 46 ralrimiva 
 |-  ( ch -> A. z e. E _pred ( z , A , R ) C_ E )
48 snex 
 |-  { x } e. _V
49 48 a1i 
 |-  ( ch -> { x } e. _V )
50 bnj893 
 |-  ( ( R _FrSe A /\ x e. A ) -> _trCl ( x , A , R ) e. _V )
51 26 15 50 syl2anc 
 |-  ( ch -> _trCl ( x , A , R ) e. _V )
52 49 51 bnj1149 
 |-  ( ch -> ( { x } u. _trCl ( x , A , R ) ) e. _V )
53 14 52 eqeltrid 
 |-  ( ch -> E e. _V )
54 1 bnj1454 
 |-  ( E e. _V -> ( E e. B <-> [. E / d ]. ( d C_ A /\ A. x e. d _pred ( x , A , R ) C_ d ) ) )
55 53 54 syl 
 |-  ( ch -> ( E e. B <-> [. E / d ]. ( d C_ A /\ A. x e. d _pred ( x , A , R ) C_ d ) ) )
56 bnj602 
 |-  ( x = z -> _pred ( x , A , R ) = _pred ( z , A , R ) )
57 56 sseq1d 
 |-  ( x = z -> ( _pred ( x , A , R ) C_ d <-> _pred ( z , A , R ) C_ d ) )
58 57 cbvralvw 
 |-  ( A. x e. d _pred ( x , A , R ) C_ d <-> A. z e. d _pred ( z , A , R ) C_ d )
59 58 anbi2i 
 |-  ( ( d C_ A /\ A. x e. d _pred ( x , A , R ) C_ d ) <-> ( d C_ A /\ A. z e. d _pred ( z , A , R ) C_ d ) )
60 59 sbcbii 
 |-  ( [. E / d ]. ( d C_ A /\ A. x e. d _pred ( x , A , R ) C_ d ) <-> [. E / d ]. ( d C_ A /\ A. z e. d _pred ( z , A , R ) C_ d ) )
61 55 60 bitrdi 
 |-  ( ch -> ( E e. B <-> [. E / d ]. ( d C_ A /\ A. z e. d _pred ( z , A , R ) C_ d ) ) )
62 sseq1 
 |-  ( d = E -> ( d C_ A <-> E C_ A ) )
63 sseq2 
 |-  ( d = E -> ( _pred ( z , A , R ) C_ d <-> _pred ( z , A , R ) C_ E ) )
64 63 raleqbi1dv 
 |-  ( d = E -> ( A. z e. d _pred ( z , A , R ) C_ d <-> A. z e. E _pred ( z , A , R ) C_ E ) )
65 62 64 anbi12d 
 |-  ( d = E -> ( ( d C_ A /\ A. z e. d _pred ( z , A , R ) C_ d ) <-> ( E C_ A /\ A. z e. E _pred ( z , A , R ) C_ E ) ) )
66 65 sbcieg 
 |-  ( E e. _V -> ( [. E / d ]. ( d C_ A /\ A. z e. d _pred ( z , A , R ) C_ d ) <-> ( E C_ A /\ A. z e. E _pred ( z , A , R ) C_ E ) ) )
67 53 66 syl 
 |-  ( ch -> ( [. E / d ]. ( d C_ A /\ A. z e. d _pred ( z , A , R ) C_ d ) <-> ( E C_ A /\ A. z e. E _pred ( z , A , R ) C_ E ) ) )
68 61 67 bitrd 
 |-  ( ch -> ( E e. B <-> ( E C_ A /\ A. z e. E _pred ( z , A , R ) C_ E ) ) )
69 20 47 68 mpbir2and 
 |-  ( ch -> E e. B )