Metamath Proof Explorer


Theorem bnj1136

Description: Technical lemma for bnj69 . 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 bnj1136.1 B = pred X A R y trCl X A R trCl y A R
bnj1136.2 θ R FrSe A X A
bnj1136.3 τ B V TrFo B A R pred X A R B
Assertion bnj1136 R FrSe A X A trCl X A R = B

Proof

Step Hyp Ref Expression
1 bnj1136.1 B = pred X A R y trCl X A R trCl y A R
2 bnj1136.2 θ R FrSe A X A
3 bnj1136.3 τ B V TrFo B A R pred X A R B
4 2 biimpri R FrSe A X A θ
5 bnj1148 R FrSe A X A pred X A R V
6 bnj893 R FrSe A X A trCl X A R V
7 simp1 R FrSe A X A y trCl X A R R FrSe A
8 bnj1127 y trCl X A R y A
9 8 3ad2ant3 R FrSe A X A y trCl X A R y A
10 bnj893 R FrSe A y A trCl y A R V
11 7 9 10 syl2anc R FrSe A X A y trCl X A R trCl y A R V
12 11 3expia R FrSe A X A y trCl X A R trCl y A R V
13 12 ralrimiv R FrSe A X A y trCl X A R trCl y A R V
14 iunexg trCl X A R V y trCl X A R trCl y A R V y trCl X A R trCl y A R V
15 6 13 14 syl2anc R FrSe A X A y trCl X A R trCl y A R V
16 5 15 bnj1149 R FrSe A X A pred X A R y trCl X A R trCl y A R V
17 1 16 eqeltrid R FrSe A X A B V
18 1 bnj1137 R FrSe A X A TrFo B A R
19 1 bnj931 pred X A R B
20 19 a1i R FrSe A X A pred X A R B
21 17 18 20 3 syl3anbrc R FrSe A X A τ
22 2 3 bnj1124 θ τ trCl X A R B
23 4 21 22 syl2anc R FrSe A X A trCl X A R B
24 bnj906 R FrSe A X A pred X A R trCl X A R
25 bnj1125 R FrSe A X A y trCl X A R trCl y A R trCl X A R
26 25 3expia R FrSe A X A y trCl X A R trCl y A R trCl X A R
27 26 ralrimiv R FrSe A X A y trCl X A R trCl y A R trCl X A R
28 ss2iun y trCl X A R trCl y A R trCl X A R y trCl X A R trCl y A R y trCl X A R trCl X A R
29 bnj1143 y trCl X A R trCl X A R trCl X A R
30 28 29 sstrdi y trCl X A R trCl y A R trCl X A R y trCl X A R trCl y A R trCl X A R
31 27 30 syl R FrSe A X A y trCl X A R trCl y A R trCl X A R
32 24 31 unssd R FrSe A X A pred X A R y trCl X A R trCl y A R trCl X A R
33 1 32 eqsstrid R FrSe A X A B trCl X A R
34 23 33 eqssd R FrSe A X A trCl X A R = B