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.

		Ref	Expression
	Assertion	tratrbVD	$⊢ (Tr A \land \forall x \in A \forall y \in A (x \in y \lor y \in x \lor x = y) \land B \in A) \to Tr B$

Proof

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

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 )

Metamath Proof Explorer

Theorem tratrbVD

Proof