Metamath Proof Explorer


Theorem tratrbVD

Description: Virtual deduction proof of tratrb . The following user's proof is completed by invoking mmj2's unify command and using mmj2's StepSelector to pick all remaining steps of the Metamath proof.

1:: |- (. ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) ->. ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) ).
2:1,?: e1a |- (. ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) ->. Tr A ).
3:1,?: e1a |- (. ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) ->. A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) ).
4:1,?: e1a |- (. ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) ->. B e. A ).
5:: |- (. ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) , ( x e. y /\ y e. B ) ->. ( x e. y /\ y e. B ) ).
6:5,?: e2 |- (. ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) , ( x e. y /\ y e. B ) ->. x e. y ).
7:5,?: e2 |- (. ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) , ( x e. y /\ y e. B ) ->. y e. B ).
8:2,7,4,?: e121 |- (. ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) , ( x e. y /\ y e. B ) ->. y e. A ).
9:2,6,8,?: e122 |- (. ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) , ( x e. y /\ y e. B ) ->. x e. A ).
10:: |- (. ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) , ( x e. y /\ y e. B ) , B e. x ->. B e. x ).
11:6,7,10,?: e223 |- (. ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) , ( x e. y /\ y e. B ) , B e. x ->. ( x e. y /\ y e. B /\ B e. x ) ).
12:11: |- (. ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) , ( x e. y /\ y e. B ) ->. ( B e. x -> ( x e. y /\ y e. B /\ B e. x ) ) ).
13:: |- -. ( x e. y /\ y e. B /\ B e. x )
14:12,13,?: e20 |- (. ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) , ( x e. y /\ y e. B ) ->. -. B e. x ).
15:: |- (. ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) , ( x e. y /\ y e. B ) , x = B ->. x = B ).
16:7,15,?: e23 |- (. ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) , ( x e. y /\ y e. B ) , x = B ->. y e. x ).
17:6,16,?: e23 |- (. ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) , ( x e. y /\ y e. B ) , x = B ->. ( x e. y /\ y e. x ) ).
18:17: |- (. ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) , ( x e. y /\ y e. B ) ->. ( x = B -> ( x e. y /\ y e. x ) ) ).
19:: |- -. ( x e. y /\ y e. x )
20:18,19,?: e20 |- (. ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) , ( x e. y /\ y e. B ) ->. -. x = B ).
21:3,?: e1a |- (. ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) ->. A. y e. A A. x e. A ( x e. y \/ y e. x \/ x = y ) ).
22:21,9,4,?: e121 |- (. ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) , ( x e. y /\ y e. B ) ->. [. x / x ]. [. B / y ]. ( x e. y \/ y e. x \/ x = y ) ).
23:22,?: e2 |- (. ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) , ( x e. y /\ y e. B ) ->. [. B / y ]. ( x e. y \/ y e. x \/ x = y ) ).
24:4,23,?: e12 |- (. ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) , ( x e. y /\ y e. B ) ->. ( x e. B \/ B e. x \/ x = B ) ).
25:14,20,24,?: e222 |- (. ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) , ( x e. y /\ y e. B ) ->. x e. B ).
26:25: |- (. ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) ->. ( ( x e. y /\ y e. B ) -> x e. B ) ).
27:: |- ( A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) -> A. y A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) )
28:27,?: e0a |- ( ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) -> A. y ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) )
29:28,26: |- (. ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) ->. A. y ( ( x e. y /\ y e. B ) -> x e. B ) ).
30:: |- ( A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) -> A. x A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) )
31:30,?: e0a |- ( ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) -> A. x ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) )
32:31,29: |- (. ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) ->. A. x A. y ( ( x e. y /\ y e. B ) -> x e. B ) ).
33:32,?: e1a |- (. ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) ->. Tr B ).
qed:33: |- ( ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) -> Tr B )
(Contributed by Alan Sare, 31-Dec-2011) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion tratrbVD Tr A x A y A x y y x x = y B A Tr B

Proof

Step Hyp Ref Expression
1 hbra1 x A y A x y y x x = y x x A y A x y y x x = y
2 alrim3con13v x A y A x y y x x = y x x A y A x y y x x = y Tr A x A y A x y y x x = y B A x Tr A x A y A x y y x x = y B A
3 1 2 e0a Tr A x A y A x y y x x = y B A x Tr A x A y A x y y x x = y B A
4 ax-5 x A y x A
5 hbra1 y A x y y x x = y y y A x y y x x = y
6 4 5 hbral x A y A x y y x x = y y x A y A x y y x x = y
7 alrim3con13v x A y A x y y x x = y y x A y A x y y x x = y Tr A x A y A x y y x x = y B A y Tr A x A y A x y y x x = y B A
8 6 7 e0a Tr A x A y A x y y x x = y B A y Tr A x A y A x y y x x = y B A
9 idn2 Tr A x A y A x y y x x = y B A , x y y B x y y B
10 simpl x y y B x y
11 9 10 e2 Tr A x A y A x y y x x = y B A , x y y B x y
12 simpr x y y B y B
13 9 12 e2 Tr A x A y A x y y x x = y B A , x y y B y B
14 idn3 Tr A x A y A x y y x x = y B A , x y y B , B x B x
15 pm3.2an3 x y y B B x x y y B B x
16 11 13 14 15 e223 Tr A x A y A x y y x x = y B A , x y y B , B x x y y B B x
17 16 in3 Tr A x A y A x y y x x = y B A , x y y B B x x y y B B x
18 en3lp ¬ x y y B B x
19 con3 B x x y y B B x ¬ x y y B B x ¬ B x
20 17 18 19 e20 Tr A x A y A x y y x x = y B A , x y y B ¬ B x
21 idn3 Tr A x A y A x y y x x = y B A , x y y B , x = B x = B
22 eleq2 x = B y x y B
23 22 biimprcd y B x = B y x
24 13 21 23 e23 Tr A x A y A x y y x x = y B A , x y y B , x = B y x
25 pm3.2 x y y x x y y x
26 11 24 25 e23 Tr A x A y A x y y x x = y B A , x y y B , x = B x y y x
27 26 in3 Tr A x A y A x y y x x = y B A , x y y B x = B x y y x
28 en2lp ¬ x y y x
29 con3 x = B x y y x ¬ x y y x ¬ x = B
30 27 28 29 e20 Tr A x A y A x y y x x = y B A , x y y B ¬ x = B
31 idn1 Tr A x A y A x y y x x = y B A Tr A x A y A x y y x x = y B A
32 simp3 Tr A x A y A x y y x x = y B A B A
33 31 32 e1a Tr A x A y A x y y x x = y B A B A
34 simp2 Tr A x A y A x y y x x = y B A x A y A x y y x x = y
35 31 34 e1a Tr A x A y A x y y x x = y B A x A y A x y y x x = y
36 ralcom x A y A x y y x x = y y A x A x y y x x = y
37 36 biimpi x A y A x y y x x = y y A x A x y y x x = y
38 35 37 e1a Tr A x A y A x y y x x = y B A y A x A x y y x x = y
39 simp1 Tr A x A y A x y y x x = y B A Tr A
40 31 39 e1a Tr A x A y A x y y x x = y B A Tr A
41 trel Tr A y B B A y A
42 41 expd Tr A y B B A y A
43 40 13 33 42 e121 Tr A x A y A x y y x x = y B A , x y y B y A
44 trel Tr A x y y A x A
45 44 expd Tr A x y y A x A
46 40 11 43 45 e122 Tr A x A y A x y y x x = y B A , x y y B x A
47 rspsbc2 B A x A y A x A x y y x x = y [˙x / x]˙ [˙B / y]˙ x y y x x = y
48 47 com13 y A x A x y y x x = y x A B A [˙x / x]˙ [˙B / y]˙ x y y x x = y
49 38 46 33 48 e121 Tr A x A y A x y y x x = y B A , x y y B [˙x / x]˙ [˙B / y]˙ x y y x x = y
50 equid x = x
51 sbceq2a x = x [˙x / x]˙ [˙B / y]˙ x y y x x = y [˙B / y]˙ x y y x x = y
52 50 51 ax-mp [˙x / x]˙ [˙B / y]˙ x y y x x = y [˙B / y]˙ x y y x x = y
53 52 biimpi [˙x / x]˙ [˙B / y]˙ x y y x x = y [˙B / y]˙ x y y x x = y
54 49 53 e2 Tr A x A y A x y y x x = y B A , x y y B [˙B / y]˙ x y y x x = y
55 sbcoreleleq B A [˙B / y]˙ x y y x x = y x B B x x = B
56 55 biimpd B A [˙B / y]˙ x y y x x = y x B B x x = B
57 33 54 56 e12 Tr A x A y A x y y x x = y B A , x y y B x B B x x = B
58 3ornot23 ¬ B x ¬ x = B x B B x x = B x B
59 58 ex ¬ B x ¬ x = B x B B x x = B x B
60 20 30 57 59 e222 Tr A x A y A x y y x x = y B A , x y y B x B
61 60 in2 Tr A x A y A x y y x x = y B A x y y B x B
62 8 61 gen11nv Tr A x A y A x y y x x = y B A y x y y B x B
63 3 62 gen11nv Tr A x A y A x y y x x = y B A x y x y y B x B
64 dftr2 Tr B x y x y y B x B
65 64 biimpri x y x y y B x B Tr B
66 63 65 e1a Tr A x A y A x y y x x = y B A Tr B
67 66 in1 Tr A x A y A x y y x x = y B A Tr B