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 /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) -> Tr B )

Proof

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