undif3VD

Description: The first equality of Exercise 13 of TakeutiZaring p. 22. Virtual deduction proof of undif3 . The following User's Proof is a Virtual Deduction proof completed automatically by the tools program completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. undif3 is undif3VD without virtual deductions and was automatically derived from undif3VD .

		Ref	Expression
	Assertion	undif3VD	\|- ( A u. ( B \ C ) ) = ( ( A u. B ) \ ( C \ A ) )

Proof

Step	Hyp	Ref	Expression
1		elun	\|- ( x e. ( A u. ( B \ C ) ) <-> ( x e. A \/ x e. ( B \ C ) ) )
2		eldif	\|- ( x e. ( B \ C ) <-> ( x e. B /\ -. x e. C ) )
3	2	orbi2i	\|- ( ( x e. A \/ x e. ( B \ C ) ) <-> ( x e. A \/ ( x e. B /\ -. x e. C ) ) )
4	1 3	bitri	\|- ( x e. ( A u. ( B \ C ) ) <-> ( x e. A \/ ( x e. B /\ -. x e. C ) ) )
5		idn1	\|- (. x e. A ->. x e. A ).
6		orc	\|- ( x e. A -> ( x e. A \/ x e. B ) )
7	5 6	e1a	\|- (. x e. A ->. ( x e. A \/ x e. B ) ).
8		olc	\|- ( x e. A -> ( -. x e. C \/ x e. A ) )
9	5 8	e1a	\|- (. x e. A ->. ( -. x e. C \/ x e. A ) ).
10		pm3.2	\|- ( ( x e. A \/ x e. B ) -> ( ( -. x e. C \/ x e. A ) -> ( ( x e. A \/ x e. B ) /\ ( -. x e. C \/ x e. A ) ) ) )
11	7 9 10	e11	\|- (. x e. A ->. ( ( x e. A \/ x e. B ) /\ ( -. x e. C \/ x e. A ) ) ).
12	11	in1	\|- ( x e. A -> ( ( x e. A \/ x e. B ) /\ ( -. x e. C \/ x e. A ) ) )
13		idn1	\|- (. ( x e. B /\ -. x e. C ) ->. ( x e. B /\ -. x e. C ) ).
14		simpl	\|- ( ( x e. B /\ -. x e. C ) -> x e. B )
15	13 14	e1a	\|- (. ( x e. B /\ -. x e. C ) ->. x e. B ).
16		olc	\|- ( x e. B -> ( x e. A \/ x e. B ) )
17	15 16	e1a	\|- (. ( x e. B /\ -. x e. C ) ->. ( x e. A \/ x e. B ) ).
18		simpr	\|- ( ( x e. B /\ -. x e. C ) -> -. x e. C )
19	13 18	e1a	\|- (. ( x e. B /\ -. x e. C ) ->. -. x e. C ).
20		orc	\|- ( -. x e. C -> ( -. x e. C \/ x e. A ) )
21	19 20	e1a	\|- (. ( x e. B /\ -. x e. C ) ->. ( -. x e. C \/ x e. A ) ).
22	17 21 10	e11	\|- (. ( x e. B /\ -. x e. C ) ->. ( ( x e. A \/ x e. B ) /\ ( -. x e. C \/ x e. A ) ) ).
23	22	in1	\|- ( ( x e. B /\ -. x e. C ) -> ( ( x e. A \/ x e. B ) /\ ( -. x e. C \/ x e. A ) ) )
24	12 23	jaoi	\|- ( ( x e. A \/ ( x e. B /\ -. x e. C ) ) -> ( ( x e. A \/ x e. B ) /\ ( -. x e. C \/ x e. A ) ) )
25		anddi	\|- ( ( ( x e. A \/ x e. B ) /\ ( -. x e. C \/ x e. A ) ) <-> ( ( ( x e. A /\ -. x e. C ) \/ ( x e. A /\ x e. A ) ) \/ ( ( x e. B /\ -. x e. C ) \/ ( x e. B /\ x e. A ) ) ) )
26	25	bicomi	\|- ( ( ( ( x e. A /\ -. x e. C ) \/ ( x e. A /\ x e. A ) ) \/ ( ( x e. B /\ -. x e. C ) \/ ( x e. B /\ x e. A ) ) ) <-> ( ( x e. A \/ x e. B ) /\ ( -. x e. C \/ x e. A ) ) )
27		idn1	\|- (. ( x e. A /\ -. x e. C ) ->. ( x e. A /\ -. x e. C ) ).
28		simpl	\|- ( ( x e. A /\ -. x e. C ) -> x e. A )
29	28	orcd	\|- ( ( x e. A /\ -. x e. C ) -> ( x e. A \/ ( x e. B /\ -. x e. C ) ) )
30	27 29	e1a	\|- (. ( x e. A /\ -. x e. C ) ->. ( x e. A \/ ( x e. B /\ -. x e. C ) ) ).
31	30	in1	\|- ( ( x e. A /\ -. x e. C ) -> ( x e. A \/ ( x e. B /\ -. x e. C ) ) )
32		idn1	\|- (. ( x e. A /\ x e. A ) ->. ( x e. A /\ x e. A ) ).
33		simpl	\|- ( ( x e. A /\ x e. A ) -> x e. A )
34	32 33	e1a	\|- (. ( x e. A /\ x e. A ) ->. x e. A ).
35		orc	\|- ( x e. A -> ( x e. A \/ ( x e. B /\ -. x e. C ) ) )
36	34 35	e1a	\|- (. ( x e. A /\ x e. A ) ->. ( x e. A \/ ( x e. B /\ -. x e. C ) ) ).
37	36	in1	\|- ( ( x e. A /\ x e. A ) -> ( x e. A \/ ( x e. B /\ -. x e. C ) ) )
38	31 37	jaoi	\|- ( ( ( x e. A /\ -. x e. C ) \/ ( x e. A /\ x e. A ) ) -> ( x e. A \/ ( x e. B /\ -. x e. C ) ) )
39		olc	\|- ( ( x e. B /\ -. x e. C ) -> ( x e. A \/ ( x e. B /\ -. x e. C ) ) )
40	13 39	e1a	\|- (. ( x e. B /\ -. x e. C ) ->. ( x e. A \/ ( x e. B /\ -. x e. C ) ) ).
41	40	in1	\|- ( ( x e. B /\ -. x e. C ) -> ( x e. A \/ ( x e. B /\ -. x e. C ) ) )
42		idn1	\|- (. ( x e. B /\ x e. A ) ->. ( x e. B /\ x e. A ) ).
43		simpr	\|- ( ( x e. B /\ x e. A ) -> x e. A )
44	42 43	e1a	\|- (. ( x e. B /\ x e. A ) ->. x e. A ).
45	44 35	e1a	\|- (. ( x e. B /\ x e. A ) ->. ( x e. A \/ ( x e. B /\ -. x e. C ) ) ).
46	45	in1	\|- ( ( x e. B /\ x e. A ) -> ( x e. A \/ ( x e. B /\ -. x e. C ) ) )
47	41 46	jaoi	\|- ( ( ( x e. B /\ -. x e. C ) \/ ( x e. B /\ x e. A ) ) -> ( x e. A \/ ( x e. B /\ -. x e. C ) ) )
48	38 47	jaoi	\|- ( ( ( ( x e. A /\ -. x e. C ) \/ ( x e. A /\ x e. A ) ) \/ ( ( x e. B /\ -. x e. C ) \/ ( x e. B /\ x e. A ) ) ) -> ( x e. A \/ ( x e. B /\ -. x e. C ) ) )
49	26 48	sylbir	\|- ( ( ( x e. A \/ x e. B ) /\ ( -. x e. C \/ x e. A ) ) -> ( x e. A \/ ( x e. B /\ -. x e. C ) ) )
50	24 49	impbii	\|- ( ( x e. A \/ ( x e. B /\ -. x e. C ) ) <-> ( ( x e. A \/ x e. B ) /\ ( -. x e. C \/ x e. A ) ) )
51	4 50	bitri	\|- ( x e. ( A u. ( B \ C ) ) <-> ( ( x e. A \/ x e. B ) /\ ( -. x e. C \/ x e. A ) ) )
52		eldif	\|- ( x e. ( ( A u. B ) \ ( C \ A ) ) <-> ( x e. ( A u. B ) /\ -. x e. ( C \ A ) ) )
53		elun	\|- ( x e. ( A u. B ) <-> ( x e. A \/ x e. B ) )
54		eldif	\|- ( x e. ( C \ A ) <-> ( x e. C /\ -. x e. A ) )
55	54	notbii	\|- ( -. x e. ( C \ A ) <-> -. ( x e. C /\ -. x e. A ) )
56		pm4.53	\|- ( -. ( x e. C /\ -. x e. A ) <-> ( -. x e. C \/ x e. A ) )
57	55 56	bitri	\|- ( -. x e. ( C \ A ) <-> ( -. x e. C \/ x e. A ) )
58	53 57	anbi12i	\|- ( ( x e. ( A u. B ) /\ -. x e. ( C \ A ) ) <-> ( ( x e. A \/ x e. B ) /\ ( -. x e. C \/ x e. A ) ) )
59	52 58	bitri	\|- ( x e. ( ( A u. B ) \ ( C \ A ) ) <-> ( ( x e. A \/ x e. B ) /\ ( -. x e. C \/ x e. A ) ) )
60	51 59	bitr4i	\|- ( x e. ( A u. ( B \ C ) ) <-> x e. ( ( A u. B ) \ ( C \ A ) ) )
61	60	ax-gen	\|- A. x ( x e. ( A u. ( B \ C ) ) <-> x e. ( ( A u. B ) \ ( C \ A ) ) )
62		dfcleq	\|- ( ( A u. ( B \ C ) ) = ( ( A u. B ) \ ( C \ A ) ) <-> A. x ( x e. ( A u. ( B \ C ) ) <-> x e. ( ( A u. B ) \ ( C \ A ) ) ) )
63	62	biimpri	\|- ( A. x ( x e. ( A u. ( B \ C ) ) <-> x e. ( ( A u. B ) \ ( C \ A ) ) ) -> ( A u. ( B \ C ) ) = ( ( A u. B ) \ ( C \ A ) ) )
64	61 63	e0a	\|- ( A u. ( B \ C ) ) = ( ( A u. B ) \ ( C \ A ) )

1::	\|- ( x e. ( A u. ( B \ C ) ) <-> ( x e. A \/ x e. ( B \ C ) ) )
2::	\|- ( x e. ( B \ C ) <-> ( x e. B /\ -. x e. C ) )
3:2:	\|- ( ( x e. A \/ x e. ( B \ C ) ) <-> ( x e. A \/ ( x e. B /\ -. x e. C ) ) )
4:1,3:	\|- ( x e. ( A u. ( B \ C ) ) <-> ( x e. A \/ ( x e. B /\ -. x e. C ) ) )
5::	\|- (. x e. A ->. x e. A ).
6:5:	\|- (. x e. A ->. ( x e. A \/ x e. B ) ).
7:5:	\|- (. x e. A ->. ( -. x e. C \/ x e. A ) ).
8:6,7:	\|- (. x e. A ->. ( ( x e. A \/ x e. B ) /\ ( -. x e. C \/ x e. A ) ) ).
9:8:	\|- ( x e. A -> ( ( x e. A \/ x e. B ) /\ ( -. x e. C \/ x e. A ) ) )
10::	\|- (. ( x e. B /\ -. x e. C ) ->. ( x e. B /\ -. x e. C ) ).
11:10:	\|- (. ( x e. B /\ -. x e. C ) ->. x e. B ).
12:10:	\|- (. ( x e. B /\ -. x e. C ) ->. -. x e. C ).
13:11:	\|- (. ( x e. B /\ -. x e. C ) ->. ( x e. A \/ x e. B ) ).
14:12:	\|- (. ( x e. B /\ -. x e. C ) ->. ( -. x e. C \/ x e. A ) ).
15:13,14:	\|- (. ( x e. B /\ -. x e. C ) ->. ( ( x e. A \/ x e. B ) /\ ( -. x e. C \/ x e. A ) ) ).
16:15:	\|- ( ( x e. B /\ -. x e. C ) -> ( ( x e. A \/ x e. B ) /\ ( -. x e. C \/ x e. A ) ) )
17:9,16:	\|- ( ( x e. A \/ ( x e. B /\ -. x e. C ) ) -> ( ( x e. A \/ x e. B ) /\ ( -. x e. C \/ x e. A ) ) )
18::	\|- (. ( x e. A /\ -. x e. C ) ->. ( x e. A /\ -. x e. C ) ).
19:18:	\|- (. ( x e. A /\ -. x e. C ) ->. x e. A ).
20:18:	\|- (. ( x e. A /\ -. x e. C ) ->. -. x e. C ).
21:18:	\|- (. ( x e. A /\ -. x e. C ) ->. ( x e. A \/ ( x e. B /\ -. x e. C ) ) ).
22:21:	\|- ( ( x e. A /\ -. x e. C ) -> ( x e. A \/ ( x e. B /\ -. x e. C ) ) )
23::	\|- (. ( x e. A /\ x e. A ) ->. ( x e. A /\ x e. A ) ).
24:23:	\|- (. ( x e. A /\ x e. A ) ->. x e. A ).
25:24:	\|- (. ( x e. A /\ x e. A ) ->. ( x e. A \/ ( x e. B /\ -. x e. C ) ) ).
26:25:	\|- ( ( x e. A /\ x e. A ) -> ( x e. A \/ ( x e. B /\ -. x e. C ) ) )
27:10:	\|- (. ( x e. B /\ -. x e. C ) ->. ( x e. A \/ ( x e. B /\ -. x e. C ) ) ).
28:27:	\|- ( ( x e. B /\ -. x e. C ) -> ( x e. A \/ ( x e. B /\ -. x e. C ) ) )
29::	\|- (. ( x e. B /\ x e. A ) ->. ( x e. B /\ x e. A ) ).
30:29:	\|- (. ( x e. B /\ x e. A ) ->. x e. A ).
31:30:	\|- (. ( x e. B /\ x e. A ) ->. ( x e. A \/ ( x e. B /\ -. x e. C ) ) ).
32:31:	\|- ( ( x e. B /\ x e. A ) -> ( x e. A \/ ( x e. B /\ -. x e. C ) ) )
33:22,26:	\|- ( ( ( x e. A /\ -. x e. C ) \/ ( x e. A /\ x e. A ) ) -> ( x e. A \/ ( x e. B /\ -. x e. C ) ) )
34:28,32:	\|- ( ( ( x e. B /\ -. x e. C ) \/ ( x e. B /\ x e. A ) ) -> ( x e. A \/ ( x e. B /\ -. x e. C ) ) )
35:33,34:	\|- ( ( ( ( x e. A /\ -. x e. C ) \/ ( x e. A /\ x e. A ) ) \/ ( ( x e. B /\ -. x e. C ) \/ ( x e. B /\ x e. A ) ) ) -> ( x e. A \/ ( x e. B /\ -. x e. C ) ) )
36::	\|- ( ( ( ( x e. A /\ -. x e. C ) \/ ( x e. A /\ x e. A ) ) \/ ( ( x e. B /\ -. x e. C ) \/ ( x e. B /\ x e. A ) ) ) <-> ( ( x e. A \/ x e. B ) /\ ( -. x e. C \/ x e. A ) ) )
37:36,35:	\|- ( ( ( x e. A \/ x e. B ) /\ ( -. x e. C \/ x e. A ) ) -> ( x e. A \/ ( x e. B /\ -. x e. C ) ) )
38:17,37:	\|- ( ( x e. A \/ ( x e. B /\ -. x e. C ) ) <-> ( ( x e. A \/ x e. B ) /\ ( -. x e. C \/ x e. A ) ) )
39::	\|- ( x e. ( C \ A ) <-> ( x e. C /\ -. x e. A ) )
40:39:	\|- ( -. x e. ( C \ A ) <-> -. ( x e. C /\ -. x e. A ) )
41::	\|- ( -. ( x e. C /\ -. x e. A ) <-> ( -. x e. C \/ x e. A ) )
42:40,41:	\|- ( -. x e. ( C \ A ) <-> ( -. x e. C \/ x e. A ) )
43::	\|- ( x e. ( A u. B ) <-> ( x e. A \/ x e. B ) )
44:43,42:	\|- ( ( x e. ( A u. B ) /\ -. x e. ( C \ A ) ) <-> ( ( x e. A \/ x e. B ) /\ ( -. x e. C /\ x e. A ) ) )
45::	\|- ( x e. ( ( A u. B ) \ ( C \ A ) ) <-> ( x e. ( A u. B ) /\ -. x e. ( C \ A ) ) )
46:45,44:	\|- ( x e. ( ( A u. B ) \ ( C \ A ) ) <-> ( ( x e. A \/ x e. B ) /\ ( -. x e. C \/ x e. A ) ) )
47:4,38:	\|- ( x e. ( A u. ( B \ C ) ) <-> ( ( x e. A \/ x e. B ) /\ ( -. x e. C \/ x e. A ) ) )
48:46,47:	\|- ( x e. ( A u. ( B \ C ) ) <-> x e. ( ( A u. B ) \ ( C \ A ) ) )
49:48:	\|- A. x ( x e. ( A u. ( B \ C ) ) <-> x e. ( ( A u. B ) \ ( C \ A ) ) )
qed:49:	\|- ( A u. ( B \ C ) ) = ( ( A u. B ) \ ( C \ A ) )

Metamath Proof Explorer

Theorem undif3VD

Proof