Users' Mathboxes Mathbox for Alan Sare < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  undif3VD Structured version   Visualization version   GIF version

Theorem undif3VD 42175
Description: The first equality of Exercise 13 of [TakeutiZaring] p. 22. Virtual deduction proof of undif3 4205. 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 4205 is undif3VD 42175 without virtual deductions and was automatically derived from undif3VD 42175.
1:: (𝑥 ∈ (𝐴 ∪ (𝐵𝐶)) ↔ (𝑥𝐴 𝑥 ∈ (𝐵𝐶)))
2:: (𝑥 ∈ (𝐵𝐶) ↔ (𝑥𝐵 ∧ ¬ 𝑥 𝐶))
3:2: ((𝑥𝐴𝑥 ∈ (𝐵𝐶)) ↔ (𝑥 𝐴 ∨ (𝑥𝐵 ∧ ¬ 𝑥𝐶)))
4:1,3: (𝑥 ∈ (𝐴 ∪ (𝐵𝐶)) ↔ (𝑥𝐴 ∨ (𝑥𝐵 ∧ ¬ 𝑥𝐶)))
5:: (   𝑥𝐴   ▶   𝑥𝐴   )
6:5: (   𝑥𝐴   ▶   (𝑥𝐴𝑥𝐵)   )
7:5: (   𝑥𝐴   ▶   𝑥𝐶𝑥𝐴)   )
8:6,7: (   𝑥𝐴   ▶   ((𝑥𝐴𝑥𝐵) ∧ 𝑥𝐶𝑥𝐴))   )
9:8: (𝑥𝐴 → ((𝑥𝐴𝑥𝐵) ∧ ( ¬ 𝑥𝐶𝑥𝐴)))
10:: (   (𝑥𝐵 ∧ ¬ 𝑥𝐶)   ▶   (𝑥𝐵 ∧ ¬ 𝑥𝐶)   )
11:10: (   (𝑥𝐵 ∧ ¬ 𝑥𝐶)   ▶   𝑥𝐵   )
12:10: (   (𝑥𝐵 ∧ ¬ 𝑥𝐶)   ▶   ¬ 𝑥𝐶    )
13:11: (   (𝑥𝐵 ∧ ¬ 𝑥𝐶)   ▶   (𝑥𝐴 𝑥𝐵)   )
14:12: (   (𝑥𝐵 ∧ ¬ 𝑥𝐶)   ▶   𝑥 𝐶𝑥𝐴)   )
15:13,14: (   (𝑥𝐵 ∧ ¬ 𝑥𝐶)   ▶   ((𝑥 𝐴𝑥𝐵) ∧ (¬ 𝑥𝐶𝑥𝐴))   )
16:15: ((𝑥𝐵 ∧ ¬ 𝑥𝐶) → ((𝑥𝐴 𝑥𝐵) ∧ (¬ 𝑥𝐶𝑥𝐴)))
17:9,16: ((𝑥𝐴 ∨ (𝑥𝐵 ∧ ¬ 𝑥𝐶)) → ((𝑥𝐴𝑥𝐵) ∧ (¬ 𝑥𝐶𝑥𝐴)))
18:: (   (𝑥𝐴 ∧ ¬ 𝑥𝐶)   ▶   (𝑥𝐴 ∧ ¬ 𝑥𝐶)   )
19:18: (   (𝑥𝐴 ∧ ¬ 𝑥𝐶)   ▶   𝑥𝐴   )
20:18: (   (𝑥𝐴 ∧ ¬ 𝑥𝐶)   ▶   ¬ 𝑥𝐶    )
21:18: (   (𝑥𝐴 ∧ ¬ 𝑥𝐶)   ▶   (𝑥𝐴 ∨ (𝑥𝐵 ∧ ¬ 𝑥𝐶))   )
22:21: ((𝑥𝐴 ∧ ¬ 𝑥𝐶) → (𝑥𝐴 (𝑥𝐵 ∧ ¬ 𝑥𝐶)))
23:: (   (𝑥𝐴𝑥𝐴)   ▶   (𝑥𝐴 𝑥𝐴)   )
24:23: (   (𝑥𝐴𝑥𝐴)   ▶   𝑥𝐴   )
25:24: (   (𝑥𝐴𝑥𝐴)   ▶   (𝑥𝐴 (𝑥𝐵 ∧ ¬ 𝑥𝐶))   )
26:25: ((𝑥𝐴𝑥𝐴) → (𝑥𝐴 ∨ ( 𝑥𝐵 ∧ ¬ 𝑥𝐶)))
27:10: (   (𝑥𝐵 ∧ ¬ 𝑥𝐶)   ▶   (𝑥𝐴 ∨ (𝑥𝐵 ∧ ¬ 𝑥𝐶))   )
28:27: ((𝑥𝐵 ∧ ¬ 𝑥𝐶) → (𝑥𝐴 (𝑥𝐵 ∧ ¬ 𝑥𝐶)))
29:: (   (𝑥𝐵𝑥𝐴)   ▶   (𝑥𝐵 𝑥𝐴)   )
30:29: (   (𝑥𝐵𝑥𝐴)   ▶   𝑥𝐴   )
31:30: (   (𝑥𝐵𝑥𝐴)   ▶   (𝑥𝐴 (𝑥𝐵 ∧ ¬ 𝑥𝐶))   )
32:31: ((𝑥𝐵𝑥𝐴) → (𝑥𝐴 ∨ ( 𝑥𝐵 ∧ ¬ 𝑥𝐶)))
33:22,26: (((𝑥𝐴 ∧ ¬ 𝑥𝐶) ∨ (𝑥𝐴 𝑥𝐴)) → (𝑥𝐴 ∨ (𝑥𝐵 ∧ ¬ 𝑥𝐶)))
34:28,32: (((𝑥𝐵 ∧ ¬ 𝑥𝐶) ∨ (𝑥𝐵 𝑥𝐴)) → (𝑥𝐴 ∨ (𝑥𝐵 ∧ ¬ 𝑥𝐶)))
35:33,34: ((((𝑥𝐴 ∧ ¬ 𝑥𝐶) ∨ (𝑥 𝐴𝑥𝐴)) ∨ ((𝑥𝐵 ∧ ¬ 𝑥𝐶) ∨ (𝑥𝐵𝑥𝐴))) → (𝑥𝐴 ∨ (𝑥𝐵 ∧ ¬ 𝑥𝐶)))
36:: ((((𝑥𝐴 ∧ ¬ 𝑥𝐶) ∨ (𝑥 𝐴𝑥𝐴)) ∨ ((𝑥𝐵 ∧ ¬ 𝑥𝐶) ∨ (𝑥𝐵𝑥𝐴))) ↔ ((𝑥𝐴𝑥𝐵) ∧ (¬ 𝑥𝐶𝑥𝐴)))
37:36,35: (((𝑥𝐴𝑥𝐵) ∧ (¬ 𝑥𝐶 𝑥𝐴)) → (𝑥𝐴 ∨ (𝑥𝐵 ∧ ¬ 𝑥𝐶)))
38:17,37: ((𝑥𝐴 ∨ (𝑥𝐵 ∧ ¬ 𝑥𝐶)) ↔ ((𝑥𝐴𝑥𝐵) ∧ (¬ 𝑥𝐶𝑥𝐴)))
39:: (𝑥 ∈ (𝐶𝐴) ↔ (𝑥𝐶 ∧ ¬ 𝑥 𝐴))
40:39: 𝑥 ∈ (𝐶𝐴) ↔ ¬ (𝑥𝐶 ¬ 𝑥𝐴))
41:: (¬ (𝑥𝐶 ∧ ¬ 𝑥𝐴) ↔ (¬ 𝑥 𝐶𝑥𝐴))
42:40,41: 𝑥 ∈ (𝐶𝐴) ↔ (¬ 𝑥𝐶𝑥 𝐴))
43:: (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴𝑥𝐵 ))
44:43,42: ((𝑥 ∈ (𝐴𝐵) ∧ ¬ 𝑥 ∈ (𝐶𝐴) ) ↔ ((𝑥𝐴𝑥𝐵) ∧ (¬ 𝑥𝐶𝑥𝐴)))
45:: (𝑥 ∈ ((𝐴𝐵) ∖ (𝐶𝐴)) ↔ ( 𝑥 ∈ (𝐴𝐵) ∧ ¬ 𝑥 ∈ (𝐶𝐴)))
46:45,44: (𝑥 ∈ ((𝐴𝐵) ∖ (𝐶𝐴)) ↔ ( (𝑥𝐴𝑥𝐵) ∧ (¬ 𝑥𝐶𝑥𝐴)))
47:4,38: (𝑥 ∈ (𝐴 ∪ (𝐵𝐶)) ↔ ((𝑥𝐴 𝑥𝐵) ∧ (¬ 𝑥𝐶𝑥𝐴)))
48:46,47: (𝑥 ∈ (𝐴 ∪ (𝐵𝐶)) ↔ 𝑥 ∈ ((𝐴 𝐵) ∖ (𝐶𝐴)))
49:48: 𝑥(𝑥 ∈ (𝐴 ∪ (𝐵𝐶)) ↔ 𝑥 ((𝐴𝐵) ∖ (𝐶𝐴)))
qed:49: (𝐴 ∪ (𝐵𝐶)) = ((𝐴𝐵) ∖ (𝐶 𝐴))
(Contributed by Alan Sare, 17-Apr-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
undif3VD (𝐴 ∪ (𝐵𝐶)) = ((𝐴𝐵) ∖ (𝐶𝐴))

Proof of Theorem undif3VD
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 elun 4063 . . . . . 6 (𝑥 ∈ (𝐴 ∪ (𝐵𝐶)) ↔ (𝑥𝐴𝑥 ∈ (𝐵𝐶)))
2 eldif 3876 . . . . . . 7 (𝑥 ∈ (𝐵𝐶) ↔ (𝑥𝐵 ∧ ¬ 𝑥𝐶))
32orbi2i 913 . . . . . 6 ((𝑥𝐴𝑥 ∈ (𝐵𝐶)) ↔ (𝑥𝐴 ∨ (𝑥𝐵 ∧ ¬ 𝑥𝐶)))
41, 3bitri 278 . . . . 5 (𝑥 ∈ (𝐴 ∪ (𝐵𝐶)) ↔ (𝑥𝐴 ∨ (𝑥𝐵 ∧ ¬ 𝑥𝐶)))
5 idn1 41867 . . . . . . . . . 10 (   𝑥𝐴   ▶   𝑥𝐴   )
6 orc 867 . . . . . . . . . 10 (𝑥𝐴 → (𝑥𝐴𝑥𝐵))
75, 6e1a 41920 . . . . . . . . 9 (   𝑥𝐴   ▶   (𝑥𝐴𝑥𝐵)   )
8 olc 868 . . . . . . . . . 10 (𝑥𝐴 → (¬ 𝑥𝐶𝑥𝐴))
95, 8e1a 41920 . . . . . . . . 9 (   𝑥𝐴   ▶   𝑥𝐶𝑥𝐴)   )
10 pm3.2 473 . . . . . . . . 9 ((𝑥𝐴𝑥𝐵) → ((¬ 𝑥𝐶𝑥𝐴) → ((𝑥𝐴𝑥𝐵) ∧ (¬ 𝑥𝐶𝑥𝐴))))
117, 9, 10e11 41981 . . . . . . . 8 (   𝑥𝐴   ▶   ((𝑥𝐴𝑥𝐵) ∧ (¬ 𝑥𝐶𝑥𝐴))   )
1211in1 41864 . . . . . . 7 (𝑥𝐴 → ((𝑥𝐴𝑥𝐵) ∧ (¬ 𝑥𝐶𝑥𝐴)))
13 idn1 41867 . . . . . . . . . . 11 (   (𝑥𝐵 ∧ ¬ 𝑥𝐶)   ▶   (𝑥𝐵 ∧ ¬ 𝑥𝐶)   )
14 simpl 486 . . . . . . . . . . 11 ((𝑥𝐵 ∧ ¬ 𝑥𝐶) → 𝑥𝐵)
1513, 14e1a 41920 . . . . . . . . . 10 (   (𝑥𝐵 ∧ ¬ 𝑥𝐶)   ▶   𝑥𝐵   )
16 olc 868 . . . . . . . . . 10 (𝑥𝐵 → (𝑥𝐴𝑥𝐵))
1715, 16e1a 41920 . . . . . . . . 9 (   (𝑥𝐵 ∧ ¬ 𝑥𝐶)   ▶   (𝑥𝐴𝑥𝐵)   )
18 simpr 488 . . . . . . . . . . 11 ((𝑥𝐵 ∧ ¬ 𝑥𝐶) → ¬ 𝑥𝐶)
1913, 18e1a 41920 . . . . . . . . . 10 (   (𝑥𝐵 ∧ ¬ 𝑥𝐶)   ▶    ¬ 𝑥𝐶   )
20 orc 867 . . . . . . . . . 10 𝑥𝐶 → (¬ 𝑥𝐶𝑥𝐴))
2119, 20e1a 41920 . . . . . . . . 9 (   (𝑥𝐵 ∧ ¬ 𝑥𝐶)   ▶   𝑥𝐶𝑥𝐴)   )
2217, 21, 10e11 41981 . . . . . . . 8 (   (𝑥𝐵 ∧ ¬ 𝑥𝐶)   ▶   ((𝑥𝐴𝑥𝐵) ∧ (¬ 𝑥𝐶𝑥𝐴))   )
2322in1 41864 . . . . . . 7 ((𝑥𝐵 ∧ ¬ 𝑥𝐶) → ((𝑥𝐴𝑥𝐵) ∧ (¬ 𝑥𝐶𝑥𝐴)))
2412, 23jaoi 857 . . . . . 6 ((𝑥𝐴 ∨ (𝑥𝐵 ∧ ¬ 𝑥𝐶)) → ((𝑥𝐴𝑥𝐵) ∧ (¬ 𝑥𝐶𝑥𝐴)))
25 anddi 1011 . . . . . . . 8 (((𝑥𝐴𝑥𝐵) ∧ (¬ 𝑥𝐶𝑥𝐴)) ↔ (((𝑥𝐴 ∧ ¬ 𝑥𝐶) ∨ (𝑥𝐴𝑥𝐴)) ∨ ((𝑥𝐵 ∧ ¬ 𝑥𝐶) ∨ (𝑥𝐵𝑥𝐴))))
2625bicomi 227 . . . . . . 7 ((((𝑥𝐴 ∧ ¬ 𝑥𝐶) ∨ (𝑥𝐴𝑥𝐴)) ∨ ((𝑥𝐵 ∧ ¬ 𝑥𝐶) ∨ (𝑥𝐵𝑥𝐴))) ↔ ((𝑥𝐴𝑥𝐵) ∧ (¬ 𝑥𝐶𝑥𝐴)))
27 idn1 41867 . . . . . . . . . . 11 (   (𝑥𝐴 ∧ ¬ 𝑥𝐶)   ▶   (𝑥𝐴 ∧ ¬ 𝑥𝐶)   )
28 simpl 486 . . . . . . . . . . . 12 ((𝑥𝐴 ∧ ¬ 𝑥𝐶) → 𝑥𝐴)
2928orcd 873 . . . . . . . . . . 11 ((𝑥𝐴 ∧ ¬ 𝑥𝐶) → (𝑥𝐴 ∨ (𝑥𝐵 ∧ ¬ 𝑥𝐶)))
3027, 29e1a 41920 . . . . . . . . . 10 (   (𝑥𝐴 ∧ ¬ 𝑥𝐶)   ▶   (𝑥𝐴 ∨ (𝑥𝐵 ∧ ¬ 𝑥𝐶))   )
3130in1 41864 . . . . . . . . 9 ((𝑥𝐴 ∧ ¬ 𝑥𝐶) → (𝑥𝐴 ∨ (𝑥𝐵 ∧ ¬ 𝑥𝐶)))
32 idn1 41867 . . . . . . . . . . . 12 (   (𝑥𝐴𝑥𝐴)   ▶   (𝑥𝐴𝑥𝐴)   )
33 simpl 486 . . . . . . . . . . . 12 ((𝑥𝐴𝑥𝐴) → 𝑥𝐴)
3432, 33e1a 41920 . . . . . . . . . . 11 (   (𝑥𝐴𝑥𝐴)   ▶   𝑥𝐴   )
35 orc 867 . . . . . . . . . . 11 (𝑥𝐴 → (𝑥𝐴 ∨ (𝑥𝐵 ∧ ¬ 𝑥𝐶)))
3634, 35e1a 41920 . . . . . . . . . 10 (   (𝑥𝐴𝑥𝐴)   ▶   (𝑥𝐴 ∨ (𝑥𝐵 ∧ ¬ 𝑥𝐶))   )
3736in1 41864 . . . . . . . . 9 ((𝑥𝐴𝑥𝐴) → (𝑥𝐴 ∨ (𝑥𝐵 ∧ ¬ 𝑥𝐶)))
3831, 37jaoi 857 . . . . . . . 8 (((𝑥𝐴 ∧ ¬ 𝑥𝐶) ∨ (𝑥𝐴𝑥𝐴)) → (𝑥𝐴 ∨ (𝑥𝐵 ∧ ¬ 𝑥𝐶)))
39 olc 868 . . . . . . . . . . 11 ((𝑥𝐵 ∧ ¬ 𝑥𝐶) → (𝑥𝐴 ∨ (𝑥𝐵 ∧ ¬ 𝑥𝐶)))
4013, 39e1a 41920 . . . . . . . . . 10 (   (𝑥𝐵 ∧ ¬ 𝑥𝐶)   ▶   (𝑥𝐴 ∨ (𝑥𝐵 ∧ ¬ 𝑥𝐶))   )
4140in1 41864 . . . . . . . . 9 ((𝑥𝐵 ∧ ¬ 𝑥𝐶) → (𝑥𝐴 ∨ (𝑥𝐵 ∧ ¬ 𝑥𝐶)))
42 idn1 41867 . . . . . . . . . . . 12 (   (𝑥𝐵𝑥𝐴)   ▶   (𝑥𝐵𝑥𝐴)   )
43 simpr 488 . . . . . . . . . . . 12 ((𝑥𝐵𝑥𝐴) → 𝑥𝐴)
4442, 43e1a 41920 . . . . . . . . . . 11 (   (𝑥𝐵𝑥𝐴)   ▶   𝑥𝐴   )
4544, 35e1a 41920 . . . . . . . . . 10 (   (𝑥𝐵𝑥𝐴)   ▶   (𝑥𝐴 ∨ (𝑥𝐵 ∧ ¬ 𝑥𝐶))   )
4645in1 41864 . . . . . . . . 9 ((𝑥𝐵𝑥𝐴) → (𝑥𝐴 ∨ (𝑥𝐵 ∧ ¬ 𝑥𝐶)))
4741, 46jaoi 857 . . . . . . . 8 (((𝑥𝐵 ∧ ¬ 𝑥𝐶) ∨ (𝑥𝐵𝑥𝐴)) → (𝑥𝐴 ∨ (𝑥𝐵 ∧ ¬ 𝑥𝐶)))
4838, 47jaoi 857 . . . . . . 7 ((((𝑥𝐴 ∧ ¬ 𝑥𝐶) ∨ (𝑥𝐴𝑥𝐴)) ∨ ((𝑥𝐵 ∧ ¬ 𝑥𝐶) ∨ (𝑥𝐵𝑥𝐴))) → (𝑥𝐴 ∨ (𝑥𝐵 ∧ ¬ 𝑥𝐶)))
4926, 48sylbir 238 . . . . . 6 (((𝑥𝐴𝑥𝐵) ∧ (¬ 𝑥𝐶𝑥𝐴)) → (𝑥𝐴 ∨ (𝑥𝐵 ∧ ¬ 𝑥𝐶)))
5024, 49impbii 212 . . . . 5 ((𝑥𝐴 ∨ (𝑥𝐵 ∧ ¬ 𝑥𝐶)) ↔ ((𝑥𝐴𝑥𝐵) ∧ (¬ 𝑥𝐶𝑥𝐴)))
514, 50bitri 278 . . . 4 (𝑥 ∈ (𝐴 ∪ (𝐵𝐶)) ↔ ((𝑥𝐴𝑥𝐵) ∧ (¬ 𝑥𝐶𝑥𝐴)))
52 eldif 3876 . . . . 5 (𝑥 ∈ ((𝐴𝐵) ∖ (𝐶𝐴)) ↔ (𝑥 ∈ (𝐴𝐵) ∧ ¬ 𝑥 ∈ (𝐶𝐴)))
53 elun 4063 . . . . . 6 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴𝑥𝐵))
54 eldif 3876 . . . . . . . 8 (𝑥 ∈ (𝐶𝐴) ↔ (𝑥𝐶 ∧ ¬ 𝑥𝐴))
5554notbii 323 . . . . . . 7 𝑥 ∈ (𝐶𝐴) ↔ ¬ (𝑥𝐶 ∧ ¬ 𝑥𝐴))
56 pm4.53 986 . . . . . . 7 (¬ (𝑥𝐶 ∧ ¬ 𝑥𝐴) ↔ (¬ 𝑥𝐶𝑥𝐴))
5755, 56bitri 278 . . . . . 6 𝑥 ∈ (𝐶𝐴) ↔ (¬ 𝑥𝐶𝑥𝐴))
5853, 57anbi12i 630 . . . . 5 ((𝑥 ∈ (𝐴𝐵) ∧ ¬ 𝑥 ∈ (𝐶𝐴)) ↔ ((𝑥𝐴𝑥𝐵) ∧ (¬ 𝑥𝐶𝑥𝐴)))
5952, 58bitri 278 . . . 4 (𝑥 ∈ ((𝐴𝐵) ∖ (𝐶𝐴)) ↔ ((𝑥𝐴𝑥𝐵) ∧ (¬ 𝑥𝐶𝑥𝐴)))
6051, 59bitr4i 281 . . 3 (𝑥 ∈ (𝐴 ∪ (𝐵𝐶)) ↔ 𝑥 ∈ ((𝐴𝐵) ∖ (𝐶𝐴)))
6160ax-gen 1803 . 2 𝑥(𝑥 ∈ (𝐴 ∪ (𝐵𝐶)) ↔ 𝑥 ∈ ((𝐴𝐵) ∖ (𝐶𝐴)))
62 dfcleq 2730 . . 3 ((𝐴 ∪ (𝐵𝐶)) = ((𝐴𝐵) ∖ (𝐶𝐴)) ↔ ∀𝑥(𝑥 ∈ (𝐴 ∪ (𝐵𝐶)) ↔ 𝑥 ∈ ((𝐴𝐵) ∖ (𝐶𝐴))))
6362biimpri 231 . 2 (∀𝑥(𝑥 ∈ (𝐴 ∪ (𝐵𝐶)) ↔ 𝑥 ∈ ((𝐴𝐵) ∖ (𝐶𝐴))) → (𝐴 ∪ (𝐵𝐶)) = ((𝐴𝐵) ∖ (𝐶𝐴)))
6461, 63e0a 42065 1 (𝐴 ∪ (𝐵𝐶)) = ((𝐴𝐵) ∖ (𝐶𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 209  wa 399  wo 847  wal 1541   = wceq 1543  wcel 2110  cdif 3863  cun 3864
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-tru 1546  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3410  df-dif 3869  df-un 3871  df-vd1 41863
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator