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 )