Metamath Proof Explorer

Theorem bnj1408

Description: Technical lemma for bnj1414 . 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 bnj1408.1 
|- B = ( _pred ( X , A , R ) u. U_ y e. _pred ( X , A , R ) _trCl ( y , A , R ) )
bnj1408.2 
|- C = ( _pred ( X , A , R ) u. U_ y e. _trCl ( X , A , R ) _trCl ( y , A , R ) )
bnj1408.3 
|- ( th <-> ( R _FrSe A /\ X e. A ) )
bnj1408.4 
|- ( ta <-> ( B e. _V /\ _TrFo ( B , A , R ) /\ _pred ( X , A , R ) C_ B ) )
Assertion bnj1408 
|- ( ( R _FrSe A /\ X e. A ) -> _trCl ( X , A , R ) = B )

Proof

Step Hyp Ref Expression
1 bnj1408.1 
 |-  B = ( _pred ( X , A , R ) u. U_ y e. _pred ( X , A , R ) _trCl ( y , A , R ) )
2 bnj1408.2 
 |-  C = ( _pred ( X , A , R ) u. U_ y e. _trCl ( X , A , R ) _trCl ( y , A , R ) )
3 bnj1408.3 
 |-  ( th <-> ( R _FrSe A /\ X e. A ) )
4 bnj1408.4 
 |-  ( ta <-> ( B e. _V /\ _TrFo ( B , A , R ) /\ _pred ( X , A , R ) C_ B ) )
5 3 biimpri 
 |-  ( ( R _FrSe A /\ X e. A ) -> th )
6 1 bnj1413 
 |-  ( ( R _FrSe A /\ X e. A ) -> B e. _V )
7 simplll 
 |-  ( ( ( ( R _FrSe A /\ X e. A ) /\ z e. B ) /\ z e. _pred ( X , A , R ) ) -> R _FrSe A )
8 bnj213 
 |-  _pred ( X , A , R ) C_ A
9 8 sseli 
 |-  ( z e. _pred ( X , A , R ) -> z e. A )
10 9 adantl 
 |-  ( ( ( ( R _FrSe A /\ X e. A ) /\ z e. B ) /\ z e. _pred ( X , A , R ) ) -> z e. A )
11 bnj906 
 |-  ( ( R _FrSe A /\ z e. A ) -> _pred ( z , A , R ) C_ _trCl ( z , A , R ) )
12 7 10 11 syl2anc 
 |-  ( ( ( ( R _FrSe A /\ X e. A ) /\ z e. B ) /\ z e. _pred ( X , A , R ) ) -> _pred ( z , A , R ) C_ _trCl ( z , A , R ) )
13 bnj1318 
 |-  ( y = z -> _trCl ( y , A , R ) = _trCl ( z , A , R ) )
14 13 ssiun2s 
 |-  ( z e. _pred ( X , A , R ) -> _trCl ( z , A , R ) C_ U_ y e. _pred ( X , A , R ) _trCl ( y , A , R ) )
15 ssun4 
 |-  ( _trCl ( z , A , R ) C_ U_ y e. _pred ( X , A , R ) _trCl ( y , A , R ) -> _trCl ( z , A , R ) C_ ( _pred ( X , A , R ) u. U_ y e. _pred ( X , A , R ) _trCl ( y , A , R ) ) )
16 15 1 sseqtrrdi 
 |-  ( _trCl ( z , A , R ) C_ U_ y e. _pred ( X , A , R ) _trCl ( y , A , R ) -> _trCl ( z , A , R ) C_ B )
17 14 16 syl 
 |-  ( z e. _pred ( X , A , R ) -> _trCl ( z , A , R ) C_ B )
18 17 adantl 
 |-  ( ( ( ( R _FrSe A /\ X e. A ) /\ z e. B ) /\ z e. _pred ( X , A , R ) ) -> _trCl ( z , A , R ) C_ B )
19 12 18 sstrd 
 |-  ( ( ( ( R _FrSe A /\ X e. A ) /\ z e. B ) /\ z e. _pred ( X , A , R ) ) -> _pred ( z , A , R ) C_ B )
20 simpr 
 |-  ( ( ( ( R _FrSe A /\ X e. A ) /\ z e. B ) /\ z e. U_ y e. _pred ( X , A , R ) _trCl ( y , A , R ) ) -> z e. U_ y e. _pred ( X , A , R ) _trCl ( y , A , R ) )
21 20 bnj1405 
 |-  ( ( ( ( R _FrSe A /\ X e. A ) /\ z e. B ) /\ z e. U_ y e. _pred ( X , A , R ) _trCl ( y , A , R ) ) -> E. y e. _pred ( X , A , R ) z e. _trCl ( y , A , R ) )
22 biid 
 |-  ( ( ( ( ( R _FrSe A /\ X e. A ) /\ z e. B ) /\ z e. U_ y e. _pred ( X , A , R ) _trCl ( y , A , R ) ) /\ y e. _pred ( X , A , R ) /\ z e. _trCl ( y , A , R ) ) <-> ( ( ( ( R _FrSe A /\ X e. A ) /\ z e. B ) /\ z e. U_ y e. _pred ( X , A , R ) _trCl ( y , A , R ) ) /\ y e. _pred ( X , A , R ) /\ z e. _trCl ( y , A , R ) ) )
23 nfv 
 |-  F/ y ( R _FrSe A /\ X e. A )
24 nfcv 
 |-  F/_ y _pred ( X , A , R )
25 nfiu1 
 |-  F/_ y U_ y e. _pred ( X , A , R ) _trCl ( y , A , R )
26 24 25 nfun 
 |-  F/_ y ( _pred ( X , A , R ) u. U_ y e. _pred ( X , A , R ) _trCl ( y , A , R ) )
27 1 26 nfcxfr 
 |-  F/_ y B
28 27 nfcri 
 |-  F/ y z e. B
29 23 28 nfan 
 |-  F/ y ( ( R _FrSe A /\ X e. A ) /\ z e. B )
30 25 nfcri 
 |-  F/ y z e. U_ y e. _pred ( X , A , R ) _trCl ( y , A , R )
31 29 30 nfan 
 |-  F/ y ( ( ( R _FrSe A /\ X e. A ) /\ z e. B ) /\ z e. U_ y e. _pred ( X , A , R ) _trCl ( y , A , R ) )
32 31 nf5ri 
 |-  ( ( ( ( R _FrSe A /\ X e. A ) /\ z e. B ) /\ z e. U_ y e. _pred ( X , A , R ) _trCl ( y , A , R ) ) -> A. y ( ( ( R _FrSe A /\ X e. A ) /\ z e. B ) /\ z e. U_ y e. _pred ( X , A , R ) _trCl ( y , A , R ) ) )
33 21 22 32 bnj1521 
 |-  ( ( ( ( R _FrSe A /\ X e. A ) /\ z e. B ) /\ z e. U_ y e. _pred ( X , A , R ) _trCl ( y , A , R ) ) -> E. y ( ( ( ( R _FrSe A /\ X e. A ) /\ z e. B ) /\ z e. U_ y e. _pred ( X , A , R ) _trCl ( y , A , R ) ) /\ y e. _pred ( X , A , R ) /\ z e. _trCl ( y , A , R ) ) )
34 simplll 
 |-  ( ( ( ( R _FrSe A /\ X e. A ) /\ z e. B ) /\ z e. U_ y e. _pred ( X , A , R ) _trCl ( y , A , R ) ) -> R _FrSe A )
35 34 3ad2ant1 
 |-  ( ( ( ( ( R _FrSe A /\ X e. A ) /\ z e. B ) /\ z e. U_ y e. _pred ( X , A , R ) _trCl ( y , A , R ) ) /\ y e. _pred ( X , A , R ) /\ z e. _trCl ( y , A , R ) ) -> R _FrSe A )
36 bnj1147 
 |-  _trCl ( y , A , R ) C_ A
37 simp3 
 |-  ( ( ( ( ( R _FrSe A /\ X e. A ) /\ z e. B ) /\ z e. U_ y e. _pred ( X , A , R ) _trCl ( y , A , R ) ) /\ y e. _pred ( X , A , R ) /\ z e. _trCl ( y , A , R ) ) -> z e. _trCl ( y , A , R ) )
38 36 37 bnj1213 
 |-  ( ( ( ( ( R _FrSe A /\ X e. A ) /\ z e. B ) /\ z e. U_ y e. _pred ( X , A , R ) _trCl ( y , A , R ) ) /\ y e. _pred ( X , A , R ) /\ z e. _trCl ( y , A , R ) ) -> z e. A )
39 35 38 11 syl2anc 
 |-  ( ( ( ( ( R _FrSe A /\ X e. A ) /\ z e. B ) /\ z e. U_ y e. _pred ( X , A , R ) _trCl ( y , A , R ) ) /\ y e. _pred ( X , A , R ) /\ z e. _trCl ( y , A , R ) ) -> _pred ( z , A , R ) C_ _trCl ( z , A , R ) )
40 simp2 
 |-  ( ( ( ( ( R _FrSe A /\ X e. A ) /\ z e. B ) /\ z e. U_ y e. _pred ( X , A , R ) _trCl ( y , A , R ) ) /\ y e. _pred ( X , A , R ) /\ z e. _trCl ( y , A , R ) ) -> y e. _pred ( X , A , R ) )
41 8 40 bnj1213 
 |-  ( ( ( ( ( R _FrSe A /\ X e. A ) /\ z e. B ) /\ z e. U_ y e. _pred ( X , A , R ) _trCl ( y , A , R ) ) /\ y e. _pred ( X , A , R ) /\ z e. _trCl ( y , A , R ) ) -> y e. A )
42 bnj1125 
 |-  ( ( R _FrSe A /\ y e. A /\ z e. _trCl ( y , A , R ) ) -> _trCl ( z , A , R ) C_ _trCl ( y , A , R ) )
43 35 41 37 42 syl3anc 
 |-  ( ( ( ( ( R _FrSe A /\ X e. A ) /\ z e. B ) /\ z e. U_ y e. _pred ( X , A , R ) _trCl ( y , A , R ) ) /\ y e. _pred ( X , A , R ) /\ z e. _trCl ( y , A , R ) ) -> _trCl ( z , A , R ) C_ _trCl ( y , A , R ) )
44 39 43 sstrd 
 |-  ( ( ( ( ( R _FrSe A /\ X e. A ) /\ z e. B ) /\ z e. U_ y e. _pred ( X , A , R ) _trCl ( y , A , R ) ) /\ y e. _pred ( X , A , R ) /\ z e. _trCl ( y , A , R ) ) -> _pred ( z , A , R ) C_ _trCl ( y , A , R ) )
45 ssiun2 
 |-  ( y e. _pred ( X , A , R ) -> _trCl ( y , A , R ) C_ U_ y e. _pred ( X , A , R ) _trCl ( y , A , R ) )
46 45 3ad2ant2 
 |-  ( ( ( ( ( R _FrSe A /\ X e. A ) /\ z e. B ) /\ z e. U_ y e. _pred ( X , A , R ) _trCl ( y , A , R ) ) /\ y e. _pred ( X , A , R ) /\ z e. _trCl ( y , A , R ) ) -> _trCl ( y , A , R ) C_ U_ y e. _pred ( X , A , R ) _trCl ( y , A , R ) )
47 ssun4 
 |-  ( _trCl ( y , A , R ) C_ U_ y e. _pred ( X , A , R ) _trCl ( y , A , R ) -> _trCl ( y , A , R ) C_ ( _pred ( X , A , R ) u. U_ y e. _pred ( X , A , R ) _trCl ( y , A , R ) ) )
48 47 1 sseqtrrdi 
 |-  ( _trCl ( y , A , R ) C_ U_ y e. _pred ( X , A , R ) _trCl ( y , A , R ) -> _trCl ( y , A , R ) C_ B )
49 46 48 syl 
 |-  ( ( ( ( ( R _FrSe A /\ X e. A ) /\ z e. B ) /\ z e. U_ y e. _pred ( X , A , R ) _trCl ( y , A , R ) ) /\ y e. _pred ( X , A , R ) /\ z e. _trCl ( y , A , R ) ) -> _trCl ( y , A , R ) C_ B )
50 44 49 sstrd 
 |-  ( ( ( ( ( R _FrSe A /\ X e. A ) /\ z e. B ) /\ z e. U_ y e. _pred ( X , A , R ) _trCl ( y , A , R ) ) /\ y e. _pred ( X , A , R ) /\ z e. _trCl ( y , A , R ) ) -> _pred ( z , A , R ) C_ B )
51 33 50 bnj593 
 |-  ( ( ( ( R _FrSe A /\ X e. A ) /\ z e. B ) /\ z e. U_ y e. _pred ( X , A , R ) _trCl ( y , A , R ) ) -> E. y _pred ( z , A , R ) C_ B )
52 nfcv 
 |-  F/_ y _pred ( z , A , R )
53 52 27 nfss 
 |-  F/ y _pred ( z , A , R ) C_ B
54 53 nf5ri 
 |-  ( _pred ( z , A , R ) C_ B -> A. y _pred ( z , A , R ) C_ B )
55 51 54 bnj1397 
 |-  ( ( ( ( R _FrSe A /\ X e. A ) /\ z e. B ) /\ z e. U_ y e. _pred ( X , A , R ) _trCl ( y , A , R ) ) -> _pred ( z , A , R ) C_ B )
56 simpr 
 |-  ( ( ( R _FrSe A /\ X e. A ) /\ z e. B ) -> z e. B )
57 1 bnj1138 
 |-  ( z e. B <-> ( z e. _pred ( X , A , R ) \/ z e. U_ y e. _pred ( X , A , R ) _trCl ( y , A , R ) ) )
58 56 57 sylib 
 |-  ( ( ( R _FrSe A /\ X e. A ) /\ z e. B ) -> ( z e. _pred ( X , A , R ) \/ z e. U_ y e. _pred ( X , A , R ) _trCl ( y , A , R ) ) )
59 19 55 58 mpjaodan 
 |-  ( ( ( R _FrSe A /\ X e. A ) /\ z e. B ) -> _pred ( z , A , R ) C_ B )
60 59 ralrimiva 
 |-  ( ( R _FrSe A /\ X e. A ) -> A. z e. B _pred ( z , A , R ) C_ B )
61 df-bnj19 
 |-  ( _TrFo ( B , A , R ) <-> A. z e. B _pred ( z , A , R ) C_ B )
62 60 61 sylibr 
 |-  ( ( R _FrSe A /\ X e. A ) -> _TrFo ( B , A , R ) )
63 1 bnj931 
 |-  _pred ( X , A , R ) C_ B
64 63 a1i 
 |-  ( ( R _FrSe A /\ X e. A ) -> _pred ( X , A , R ) C_ B )
65 6 62 64 4 syl3anbrc 
 |-  ( ( R _FrSe A /\ X e. A ) -> ta )
66 3 4 bnj1124 
 |-  ( ( th /\ ta ) -> _trCl ( X , A , R ) C_ B )
67 5 65 66 syl2anc 
 |-  ( ( R _FrSe A /\ X e. A ) -> _trCl ( X , A , R ) C_ B )
68 bnj906 
 |-  ( ( R _FrSe A /\ X e. A ) -> _pred ( X , A , R ) C_ _trCl ( X , A , R ) )
69 iunss1 
 |-  ( _pred ( X , A , R ) C_ _trCl ( X , A , R ) -> U_ y e. _pred ( X , A , R ) _trCl ( y , A , R ) C_ U_ y e. _trCl ( X , A , R ) _trCl ( y , A , R ) )
70 unss2 
 |-  ( U_ y e. _pred ( X , A , R ) _trCl ( y , A , R ) C_ U_ y e. _trCl ( X , A , R ) _trCl ( y , A , R ) -> ( _pred ( X , A , R ) u. U_ y e. _pred ( X , A , R ) _trCl ( y , A , R ) ) C_ ( _pred ( X , A , R ) u. U_ y e. _trCl ( X , A , R ) _trCl ( y , A , R ) ) )
71 68 69 70 3syl 
 |-  ( ( R _FrSe A /\ X e. A ) -> ( _pred ( X , A , R ) u. U_ y e. _pred ( X , A , R ) _trCl ( y , A , R ) ) C_ ( _pred ( X , A , R ) u. U_ y e. _trCl ( X , A , R ) _trCl ( y , A , R ) ) )
72 71 1 2 3sstr4g 
 |-  ( ( R _FrSe A /\ X e. A ) -> B C_ C )
73 biid 
 |-  ( ( R _FrSe A /\ X e. A ) <-> ( R _FrSe A /\ X e. A ) )
74 biid 
 |-  ( ( C e. _V /\ _TrFo ( C , A , R ) /\ _pred ( X , A , R ) C_ C ) <-> ( C e. _V /\ _TrFo ( C , A , R ) /\ _pred ( X , A , R ) C_ C ) )
75 2 73 74 bnj1136 
 |-  ( ( R _FrSe A /\ X e. A ) -> _trCl ( X , A , R ) = C )
76 72 75 sseqtrrd 
 |-  ( ( R _FrSe A /\ X e. A ) -> B C_ _trCl ( X , A , R ) )
77 67 76 eqssd 
 |-  ( ( R _FrSe A /\ X e. A ) -> _trCl ( X , A , R ) = B )