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 37943
Description: The first equality of Exercise 13 of [TakeutiZaring] p. 22. Virtual deduction proof of undif3 3846. 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 3846 is undif3VD 37943 without virtual deductions and was automatically derived from undif3VD 37943.
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 3714 . . . . . 6 (𝑥 ∈ (𝐴 ∪ (𝐵𝐶)) ↔ (𝑥𝐴𝑥 ∈ (𝐵𝐶)))
2 eldif 3549 . . . . . . 7 (𝑥 ∈ (𝐵𝐶) ↔ (𝑥𝐵 ∧ ¬ 𝑥𝐶))
32orbi2i 539 . . . . . 6 ((𝑥𝐴𝑥 ∈ (𝐵𝐶)) ↔ (𝑥𝐴 ∨ (𝑥𝐵 ∧ ¬ 𝑥𝐶)))
41, 3bitri 262 . . . . 5 (𝑥 ∈ (𝐴 ∪ (𝐵𝐶)) ↔ (𝑥𝐴 ∨ (𝑥𝐵 ∧ ¬ 𝑥𝐶)))
5 idn1 37614 . . . . . . . . . 10 (   𝑥𝐴   ▶   𝑥𝐴   )
6 orc 398 . . . . . . . . . 10 (𝑥𝐴 → (𝑥𝐴𝑥𝐵))
75, 6e1a 37676 . . . . . . . . 9 (   𝑥𝐴   ▶   (𝑥𝐴𝑥𝐵)   )
8 olc 397 . . . . . . . . . 10 (𝑥𝐴 → (¬ 𝑥𝐶𝑥𝐴))
95, 8e1a 37676 . . . . . . . . 9 (   𝑥𝐴   ▶   𝑥𝐶𝑥𝐴)   )
10 pm3.2 461 . . . . . . . . 9 ((𝑥𝐴𝑥𝐵) → ((¬ 𝑥𝐶𝑥𝐴) → ((𝑥𝐴𝑥𝐵) ∧ (¬ 𝑥𝐶𝑥𝐴))))
117, 9, 10e11 37737 . . . . . . . 8 (   𝑥𝐴   ▶   ((𝑥𝐴𝑥𝐵) ∧ (¬ 𝑥𝐶𝑥𝐴))   )
1211in1 37611 . . . . . . 7 (𝑥𝐴 → ((𝑥𝐴𝑥𝐵) ∧ (¬ 𝑥𝐶𝑥𝐴)))
13 idn1 37614 . . . . . . . . . . 11 (   (𝑥𝐵 ∧ ¬ 𝑥𝐶)   ▶   (𝑥𝐵 ∧ ¬ 𝑥𝐶)   )
14 simpl 471 . . . . . . . . . . 11 ((𝑥𝐵 ∧ ¬ 𝑥𝐶) → 𝑥𝐵)
1513, 14e1a 37676 . . . . . . . . . 10 (   (𝑥𝐵 ∧ ¬ 𝑥𝐶)   ▶   𝑥𝐵   )
16 olc 397 . . . . . . . . . 10 (𝑥𝐵 → (𝑥𝐴𝑥𝐵))
1715, 16e1a 37676 . . . . . . . . 9 (   (𝑥𝐵 ∧ ¬ 𝑥𝐶)   ▶   (𝑥𝐴𝑥𝐵)   )
18 simpr 475 . . . . . . . . . . 11 ((𝑥𝐵 ∧ ¬ 𝑥𝐶) → ¬ 𝑥𝐶)
1913, 18e1a 37676 . . . . . . . . . 10 (   (𝑥𝐵 ∧ ¬ 𝑥𝐶)   ▶    ¬ 𝑥𝐶   )
20 orc 398 . . . . . . . . . 10 𝑥𝐶 → (¬ 𝑥𝐶𝑥𝐴))
2119, 20e1a 37676 . . . . . . . . 9 (   (𝑥𝐵 ∧ ¬ 𝑥𝐶)   ▶   𝑥𝐶𝑥𝐴)   )
2217, 21, 10e11 37737 . . . . . . . 8 (   (𝑥𝐵 ∧ ¬ 𝑥𝐶)   ▶   ((𝑥𝐴𝑥𝐵) ∧ (¬ 𝑥𝐶𝑥𝐴))   )
2322in1 37611 . . . . . . 7 ((𝑥𝐵 ∧ ¬ 𝑥𝐶) → ((𝑥𝐴𝑥𝐵) ∧ (¬ 𝑥𝐶𝑥𝐴)))
2412, 23jaoi 392 . . . . . 6 ((𝑥𝐴 ∨ (𝑥𝐵 ∧ ¬ 𝑥𝐶)) → ((𝑥𝐴𝑥𝐵) ∧ (¬ 𝑥𝐶𝑥𝐴)))
25 anddi 909 . . . . . . . 8 (((𝑥𝐴𝑥𝐵) ∧ (¬ 𝑥𝐶𝑥𝐴)) ↔ (((𝑥𝐴 ∧ ¬ 𝑥𝐶) ∨ (𝑥𝐴𝑥𝐴)) ∨ ((𝑥𝐵 ∧ ¬ 𝑥𝐶) ∨ (𝑥𝐵𝑥𝐴))))
2625bicomi 212 . . . . . . 7 ((((𝑥𝐴 ∧ ¬ 𝑥𝐶) ∨ (𝑥𝐴𝑥𝐴)) ∨ ((𝑥𝐵 ∧ ¬ 𝑥𝐶) ∨ (𝑥𝐵𝑥𝐴))) ↔ ((𝑥𝐴𝑥𝐵) ∧ (¬ 𝑥𝐶𝑥𝐴)))
27 idn1 37614 . . . . . . . . . . 11 (   (𝑥𝐴 ∧ ¬ 𝑥𝐶)   ▶   (𝑥𝐴 ∧ ¬ 𝑥𝐶)   )
28 simpl 471 . . . . . . . . . . . 12 ((𝑥𝐴 ∧ ¬ 𝑥𝐶) → 𝑥𝐴)
2928orcd 405 . . . . . . . . . . 11 ((𝑥𝐴 ∧ ¬ 𝑥𝐶) → (𝑥𝐴 ∨ (𝑥𝐵 ∧ ¬ 𝑥𝐶)))
3027, 29e1a 37676 . . . . . . . . . 10 (   (𝑥𝐴 ∧ ¬ 𝑥𝐶)   ▶   (𝑥𝐴 ∨ (𝑥𝐵 ∧ ¬ 𝑥𝐶))   )
3130in1 37611 . . . . . . . . 9 ((𝑥𝐴 ∧ ¬ 𝑥𝐶) → (𝑥𝐴 ∨ (𝑥𝐵 ∧ ¬ 𝑥𝐶)))
32 idn1 37614 . . . . . . . . . . . 12 (   (𝑥𝐴𝑥𝐴)   ▶   (𝑥𝐴𝑥𝐴)   )
33 simpl 471 . . . . . . . . . . . 12 ((𝑥𝐴𝑥𝐴) → 𝑥𝐴)
3432, 33e1a 37676 . . . . . . . . . . 11 (   (𝑥𝐴𝑥𝐴)   ▶   𝑥𝐴   )
35 orc 398 . . . . . . . . . . 11 (𝑥𝐴 → (𝑥𝐴 ∨ (𝑥𝐵 ∧ ¬ 𝑥𝐶)))
3634, 35e1a 37676 . . . . . . . . . 10 (   (𝑥𝐴𝑥𝐴)   ▶   (𝑥𝐴 ∨ (𝑥𝐵 ∧ ¬ 𝑥𝐶))   )
3736in1 37611 . . . . . . . . 9 ((𝑥𝐴𝑥𝐴) → (𝑥𝐴 ∨ (𝑥𝐵 ∧ ¬ 𝑥𝐶)))
3831, 37jaoi 392 . . . . . . . 8 (((𝑥𝐴 ∧ ¬ 𝑥𝐶) ∨ (𝑥𝐴𝑥𝐴)) → (𝑥𝐴 ∨ (𝑥𝐵 ∧ ¬ 𝑥𝐶)))
39 olc 397 . . . . . . . . . . 11 ((𝑥𝐵 ∧ ¬ 𝑥𝐶) → (𝑥𝐴 ∨ (𝑥𝐵 ∧ ¬ 𝑥𝐶)))
4013, 39e1a 37676 . . . . . . . . . 10 (   (𝑥𝐵 ∧ ¬ 𝑥𝐶)   ▶   (𝑥𝐴 ∨ (𝑥𝐵 ∧ ¬ 𝑥𝐶))   )
4140in1 37611 . . . . . . . . 9 ((𝑥𝐵 ∧ ¬ 𝑥𝐶) → (𝑥𝐴 ∨ (𝑥𝐵 ∧ ¬ 𝑥𝐶)))
42 idn1 37614 . . . . . . . . . . . 12 (   (𝑥𝐵𝑥𝐴)   ▶   (𝑥𝐵𝑥𝐴)   )
43 simpr 475 . . . . . . . . . . . 12 ((𝑥𝐵𝑥𝐴) → 𝑥𝐴)
4442, 43e1a 37676 . . . . . . . . . . 11 (   (𝑥𝐵𝑥𝐴)   ▶   𝑥𝐴   )
4544, 35e1a 37676 . . . . . . . . . 10 (   (𝑥𝐵𝑥𝐴)   ▶   (𝑥𝐴 ∨ (𝑥𝐵 ∧ ¬ 𝑥𝐶))   )
4645in1 37611 . . . . . . . . 9 ((𝑥𝐵𝑥𝐴) → (𝑥𝐴 ∨ (𝑥𝐵 ∧ ¬ 𝑥𝐶)))
4741, 46jaoi 392 . . . . . . . 8 (((𝑥𝐵 ∧ ¬ 𝑥𝐶) ∨ (𝑥𝐵𝑥𝐴)) → (𝑥𝐴 ∨ (𝑥𝐵 ∧ ¬ 𝑥𝐶)))
4838, 47jaoi 392 . . . . . . 7 ((((𝑥𝐴 ∧ ¬ 𝑥𝐶) ∨ (𝑥𝐴𝑥𝐴)) ∨ ((𝑥𝐵 ∧ ¬ 𝑥𝐶) ∨ (𝑥𝐵𝑥𝐴))) → (𝑥𝐴 ∨ (𝑥𝐵 ∧ ¬ 𝑥𝐶)))
4926, 48sylbir 223 . . . . . 6 (((𝑥𝐴𝑥𝐵) ∧ (¬ 𝑥𝐶𝑥𝐴)) → (𝑥𝐴 ∨ (𝑥𝐵 ∧ ¬ 𝑥𝐶)))
5024, 49impbii 197 . . . . 5 ((𝑥𝐴 ∨ (𝑥𝐵 ∧ ¬ 𝑥𝐶)) ↔ ((𝑥𝐴𝑥𝐵) ∧ (¬ 𝑥𝐶𝑥𝐴)))
514, 50bitri 262 . . . 4 (𝑥 ∈ (𝐴 ∪ (𝐵𝐶)) ↔ ((𝑥𝐴𝑥𝐵) ∧ (¬ 𝑥𝐶𝑥𝐴)))
52 eldif 3549 . . . . 5 (𝑥 ∈ ((𝐴𝐵) ∖ (𝐶𝐴)) ↔ (𝑥 ∈ (𝐴𝐵) ∧ ¬ 𝑥 ∈ (𝐶𝐴)))
53 elun 3714 . . . . . 6 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴𝑥𝐵))
54 eldif 3549 . . . . . . . 8 (𝑥 ∈ (𝐶𝐴) ↔ (𝑥𝐶 ∧ ¬ 𝑥𝐴))
5554notbii 308 . . . . . . 7 𝑥 ∈ (𝐶𝐴) ↔ ¬ (𝑥𝐶 ∧ ¬ 𝑥𝐴))
56 pm4.53 511 . . . . . . 7 (¬ (𝑥𝐶 ∧ ¬ 𝑥𝐴) ↔ (¬ 𝑥𝐶𝑥𝐴))
5755, 56bitri 262 . . . . . 6 𝑥 ∈ (𝐶𝐴) ↔ (¬ 𝑥𝐶𝑥𝐴))
5853, 57anbi12i 728 . . . . 5 ((𝑥 ∈ (𝐴𝐵) ∧ ¬ 𝑥 ∈ (𝐶𝐴)) ↔ ((𝑥𝐴𝑥𝐵) ∧ (¬ 𝑥𝐶𝑥𝐴)))
5952, 58bitri 262 . . . 4 (𝑥 ∈ ((𝐴𝐵) ∖ (𝐶𝐴)) ↔ ((𝑥𝐴𝑥𝐵) ∧ (¬ 𝑥𝐶𝑥𝐴)))
6051, 59bitr4i 265 . . 3 (𝑥 ∈ (𝐴 ∪ (𝐵𝐶)) ↔ 𝑥 ∈ ((𝐴𝐵) ∖ (𝐶𝐴)))
6160ax-gen 1712 . 2 𝑥(𝑥 ∈ (𝐴 ∪ (𝐵𝐶)) ↔ 𝑥 ∈ ((𝐴𝐵) ∖ (𝐶𝐴)))
62 dfcleq 2603 . . 3 ((𝐴 ∪ (𝐵𝐶)) = ((𝐴𝐵) ∖ (𝐶𝐴)) ↔ ∀𝑥(𝑥 ∈ (𝐴 ∪ (𝐵𝐶)) ↔ 𝑥 ∈ ((𝐴𝐵) ∖ (𝐶𝐴))))
6362biimpri 216 . 2 (∀𝑥(𝑥 ∈ (𝐴 ∪ (𝐵𝐶)) ↔ 𝑥 ∈ ((𝐴𝐵) ∖ (𝐶𝐴))) → (𝐴 ∪ (𝐵𝐶)) = ((𝐴𝐵) ∖ (𝐶𝐴)))
6461, 63e0a 37823 1 (𝐴 ∪ (𝐵𝐶)) = ((𝐴𝐵) ∖ (𝐶𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 194  wo 381  wa 382  wal 1472   = wceq 1474  wcel 1976  cdif 3536  cun 3537
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2232  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-v 3174  df-dif 3542  df-un 3544  df-vd1 37610
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator