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 y pred X A R trCl y A R
bnj1408.2 C = pred X A R y trCl X A R trCl y A R
bnj1408.3 θ R FrSe A X A
bnj1408.4 τ B V TrFo B A R pred X A R B
Assertion bnj1408 R FrSe A X A trCl X A R = B

Proof

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