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 44902
Description: The first equality of Exercise 13 of [TakeutiZaring] p. 22. Virtual deduction proof of undif3 4300. 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 4300 is undif3VD 44902 without virtual deductions and was automatically derived from undif3VD 44902.
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 4153 . . . . . 6 (𝑥 ∈ (𝐴 ∪ (𝐵𝐶)) ↔ (𝑥𝐴𝑥 ∈ (𝐵𝐶)))
2 eldif 3961 . . . . . . 7 (𝑥 ∈ (𝐵𝐶) ↔ (𝑥𝐵 ∧ ¬ 𝑥𝐶))
32orbi2i 913 . . . . . 6 ((𝑥𝐴𝑥 ∈ (𝐵𝐶)) ↔ (𝑥𝐴 ∨ (𝑥𝐵 ∧ ¬ 𝑥𝐶)))
41, 3bitri 275 . . . . 5 (𝑥 ∈ (𝐴 ∪ (𝐵𝐶)) ↔ (𝑥𝐴 ∨ (𝑥𝐵 ∧ ¬ 𝑥𝐶)))
5 idn1 44594 . . . . . . . . . 10 (   𝑥𝐴   ▶   𝑥𝐴   )
6 orc 868 . . . . . . . . . 10 (𝑥𝐴 → (𝑥𝐴𝑥𝐵))
75, 6e1a 44647 . . . . . . . . 9 (   𝑥𝐴   ▶   (𝑥𝐴𝑥𝐵)   )
8 olc 869 . . . . . . . . . 10 (𝑥𝐴 → (¬ 𝑥𝐶𝑥𝐴))
95, 8e1a 44647 . . . . . . . . 9 (   𝑥𝐴   ▶   𝑥𝐶𝑥𝐴)   )
10 pm3.2 469 . . . . . . . . 9 ((𝑥𝐴𝑥𝐵) → ((¬ 𝑥𝐶𝑥𝐴) → ((𝑥𝐴𝑥𝐵) ∧ (¬ 𝑥𝐶𝑥𝐴))))
117, 9, 10e11 44708 . . . . . . . 8 (   𝑥𝐴   ▶   ((𝑥𝐴𝑥𝐵) ∧ (¬ 𝑥𝐶𝑥𝐴))   )
1211in1 44591 . . . . . . 7 (𝑥𝐴 → ((𝑥𝐴𝑥𝐵) ∧ (¬ 𝑥𝐶𝑥𝐴)))
13 idn1 44594 . . . . . . . . . . 11 (   (𝑥𝐵 ∧ ¬ 𝑥𝐶)   ▶   (𝑥𝐵 ∧ ¬ 𝑥𝐶)   )
14 simpl 482 . . . . . . . . . . 11 ((𝑥𝐵 ∧ ¬ 𝑥𝐶) → 𝑥𝐵)
1513, 14e1a 44647 . . . . . . . . . 10 (   (𝑥𝐵 ∧ ¬ 𝑥𝐶)   ▶   𝑥𝐵   )
16 olc 869 . . . . . . . . . 10 (𝑥𝐵 → (𝑥𝐴𝑥𝐵))
1715, 16e1a 44647 . . . . . . . . 9 (   (𝑥𝐵 ∧ ¬ 𝑥𝐶)   ▶   (𝑥𝐴𝑥𝐵)   )
18 simpr 484 . . . . . . . . . . 11 ((𝑥𝐵 ∧ ¬ 𝑥𝐶) → ¬ 𝑥𝐶)
1913, 18e1a 44647 . . . . . . . . . 10 (   (𝑥𝐵 ∧ ¬ 𝑥𝐶)   ▶    ¬ 𝑥𝐶   )
20 orc 868 . . . . . . . . . 10 𝑥𝐶 → (¬ 𝑥𝐶𝑥𝐴))
2119, 20e1a 44647 . . . . . . . . 9 (   (𝑥𝐵 ∧ ¬ 𝑥𝐶)   ▶   𝑥𝐶𝑥𝐴)   )
2217, 21, 10e11 44708 . . . . . . . 8 (   (𝑥𝐵 ∧ ¬ 𝑥𝐶)   ▶   ((𝑥𝐴𝑥𝐵) ∧ (¬ 𝑥𝐶𝑥𝐴))   )
2322in1 44591 . . . . . . 7 ((𝑥𝐵 ∧ ¬ 𝑥𝐶) → ((𝑥𝐴𝑥𝐵) ∧ (¬ 𝑥𝐶𝑥𝐴)))
2412, 23jaoi 858 . . . . . 6 ((𝑥𝐴 ∨ (𝑥𝐵 ∧ ¬ 𝑥𝐶)) → ((𝑥𝐴𝑥𝐵) ∧ (¬ 𝑥𝐶𝑥𝐴)))
25 anddi 1013 . . . . . . . 8 (((𝑥𝐴𝑥𝐵) ∧ (¬ 𝑥𝐶𝑥𝐴)) ↔ (((𝑥𝐴 ∧ ¬ 𝑥𝐶) ∨ (𝑥𝐴𝑥𝐴)) ∨ ((𝑥𝐵 ∧ ¬ 𝑥𝐶) ∨ (𝑥𝐵𝑥𝐴))))
2625bicomi 224 . . . . . . 7 ((((𝑥𝐴 ∧ ¬ 𝑥𝐶) ∨ (𝑥𝐴𝑥𝐴)) ∨ ((𝑥𝐵 ∧ ¬ 𝑥𝐶) ∨ (𝑥𝐵𝑥𝐴))) ↔ ((𝑥𝐴𝑥𝐵) ∧ (¬ 𝑥𝐶𝑥𝐴)))
27 idn1 44594 . . . . . . . . . . 11 (   (𝑥𝐴 ∧ ¬ 𝑥𝐶)   ▶   (𝑥𝐴 ∧ ¬ 𝑥𝐶)   )
28 simpl 482 . . . . . . . . . . . 12 ((𝑥𝐴 ∧ ¬ 𝑥𝐶) → 𝑥𝐴)
2928orcd 874 . . . . . . . . . . 11 ((𝑥𝐴 ∧ ¬ 𝑥𝐶) → (𝑥𝐴 ∨ (𝑥𝐵 ∧ ¬ 𝑥𝐶)))
3027, 29e1a 44647 . . . . . . . . . 10 (   (𝑥𝐴 ∧ ¬ 𝑥𝐶)   ▶   (𝑥𝐴 ∨ (𝑥𝐵 ∧ ¬ 𝑥𝐶))   )
3130in1 44591 . . . . . . . . 9 ((𝑥𝐴 ∧ ¬ 𝑥𝐶) → (𝑥𝐴 ∨ (𝑥𝐵 ∧ ¬ 𝑥𝐶)))
32 idn1 44594 . . . . . . . . . . . 12 (   (𝑥𝐴𝑥𝐴)   ▶   (𝑥𝐴𝑥𝐴)   )
33 simpl 482 . . . . . . . . . . . 12 ((𝑥𝐴𝑥𝐴) → 𝑥𝐴)
3432, 33e1a 44647 . . . . . . . . . . 11 (   (𝑥𝐴𝑥𝐴)   ▶   𝑥𝐴   )
35 orc 868 . . . . . . . . . . 11 (𝑥𝐴 → (𝑥𝐴 ∨ (𝑥𝐵 ∧ ¬ 𝑥𝐶)))
3634, 35e1a 44647 . . . . . . . . . 10 (   (𝑥𝐴𝑥𝐴)   ▶   (𝑥𝐴 ∨ (𝑥𝐵 ∧ ¬ 𝑥𝐶))   )
3736in1 44591 . . . . . . . . 9 ((𝑥𝐴𝑥𝐴) → (𝑥𝐴 ∨ (𝑥𝐵 ∧ ¬ 𝑥𝐶)))
3831, 37jaoi 858 . . . . . . . 8 (((𝑥𝐴 ∧ ¬ 𝑥𝐶) ∨ (𝑥𝐴𝑥𝐴)) → (𝑥𝐴 ∨ (𝑥𝐵 ∧ ¬ 𝑥𝐶)))
39 olc 869 . . . . . . . . . . 11 ((𝑥𝐵 ∧ ¬ 𝑥𝐶) → (𝑥𝐴 ∨ (𝑥𝐵 ∧ ¬ 𝑥𝐶)))
4013, 39e1a 44647 . . . . . . . . . 10 (   (𝑥𝐵 ∧ ¬ 𝑥𝐶)   ▶   (𝑥𝐴 ∨ (𝑥𝐵 ∧ ¬ 𝑥𝐶))   )
4140in1 44591 . . . . . . . . 9 ((𝑥𝐵 ∧ ¬ 𝑥𝐶) → (𝑥𝐴 ∨ (𝑥𝐵 ∧ ¬ 𝑥𝐶)))
42 idn1 44594 . . . . . . . . . . . 12 (   (𝑥𝐵𝑥𝐴)   ▶   (𝑥𝐵𝑥𝐴)   )
43 simpr 484 . . . . . . . . . . . 12 ((𝑥𝐵𝑥𝐴) → 𝑥𝐴)
4442, 43e1a 44647 . . . . . . . . . . 11 (   (𝑥𝐵𝑥𝐴)   ▶   𝑥𝐴   )
4544, 35e1a 44647 . . . . . . . . . 10 (   (𝑥𝐵𝑥𝐴)   ▶   (𝑥𝐴 ∨ (𝑥𝐵 ∧ ¬ 𝑥𝐶))   )
4645in1 44591 . . . . . . . . 9 ((𝑥𝐵𝑥𝐴) → (𝑥𝐴 ∨ (𝑥𝐵 ∧ ¬ 𝑥𝐶)))
4741, 46jaoi 858 . . . . . . . 8 (((𝑥𝐵 ∧ ¬ 𝑥𝐶) ∨ (𝑥𝐵𝑥𝐴)) → (𝑥𝐴 ∨ (𝑥𝐵 ∧ ¬ 𝑥𝐶)))
4838, 47jaoi 858 . . . . . . 7 ((((𝑥𝐴 ∧ ¬ 𝑥𝐶) ∨ (𝑥𝐴𝑥𝐴)) ∨ ((𝑥𝐵 ∧ ¬ 𝑥𝐶) ∨ (𝑥𝐵𝑥𝐴))) → (𝑥𝐴 ∨ (𝑥𝐵 ∧ ¬ 𝑥𝐶)))
4926, 48sylbir 235 . . . . . 6 (((𝑥𝐴𝑥𝐵) ∧ (¬ 𝑥𝐶𝑥𝐴)) → (𝑥𝐴 ∨ (𝑥𝐵 ∧ ¬ 𝑥𝐶)))
5024, 49impbii 209 . . . . 5 ((𝑥𝐴 ∨ (𝑥𝐵 ∧ ¬ 𝑥𝐶)) ↔ ((𝑥𝐴𝑥𝐵) ∧ (¬ 𝑥𝐶𝑥𝐴)))
514, 50bitri 275 . . . 4 (𝑥 ∈ (𝐴 ∪ (𝐵𝐶)) ↔ ((𝑥𝐴𝑥𝐵) ∧ (¬ 𝑥𝐶𝑥𝐴)))
52 eldif 3961 . . . . 5 (𝑥 ∈ ((𝐴𝐵) ∖ (𝐶𝐴)) ↔ (𝑥 ∈ (𝐴𝐵) ∧ ¬ 𝑥 ∈ (𝐶𝐴)))
53 elun 4153 . . . . . 6 (𝑥 ∈ (𝐴𝐵) ↔ (𝑥𝐴𝑥𝐵))
54 eldif 3961 . . . . . . . 8 (𝑥 ∈ (𝐶𝐴) ↔ (𝑥𝐶 ∧ ¬ 𝑥𝐴))
5554notbii 320 . . . . . . 7 𝑥 ∈ (𝐶𝐴) ↔ ¬ (𝑥𝐶 ∧ ¬ 𝑥𝐴))
56 pm4.53 988 . . . . . . 7 (¬ (𝑥𝐶 ∧ ¬ 𝑥𝐴) ↔ (¬ 𝑥𝐶𝑥𝐴))
5755, 56bitri 275 . . . . . 6 𝑥 ∈ (𝐶𝐴) ↔ (¬ 𝑥𝐶𝑥𝐴))
5853, 57anbi12i 628 . . . . 5 ((𝑥 ∈ (𝐴𝐵) ∧ ¬ 𝑥 ∈ (𝐶𝐴)) ↔ ((𝑥𝐴𝑥𝐵) ∧ (¬ 𝑥𝐶𝑥𝐴)))
5952, 58bitri 275 . . . 4 (𝑥 ∈ ((𝐴𝐵) ∖ (𝐶𝐴)) ↔ ((𝑥𝐴𝑥𝐵) ∧ (¬ 𝑥𝐶𝑥𝐴)))
6051, 59bitr4i 278 . . 3 (𝑥 ∈ (𝐴 ∪ (𝐵𝐶)) ↔ 𝑥 ∈ ((𝐴𝐵) ∖ (𝐶𝐴)))
6160ax-gen 1795 . 2 𝑥(𝑥 ∈ (𝐴 ∪ (𝐵𝐶)) ↔ 𝑥 ∈ ((𝐴𝐵) ∖ (𝐶𝐴)))
62 dfcleq 2730 . . 3 ((𝐴 ∪ (𝐵𝐶)) = ((𝐴𝐵) ∖ (𝐶𝐴)) ↔ ∀𝑥(𝑥 ∈ (𝐴 ∪ (𝐵𝐶)) ↔ 𝑥 ∈ ((𝐴𝐵) ∖ (𝐶𝐴))))
6362biimpri 228 . 2 (∀𝑥(𝑥 ∈ (𝐴 ∪ (𝐵𝐶)) ↔ 𝑥 ∈ ((𝐴𝐵) ∖ (𝐶𝐴))) → (𝐴 ∪ (𝐵𝐶)) = ((𝐴𝐵) ∖ (𝐶𝐴)))
6461, 63e0a 44792 1 (𝐴 ∪ (𝐵𝐶)) = ((𝐴𝐵) ∖ (𝐶𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 206  wa 395  wo 848  wal 1538   = wceq 1540  wcel 2108  cdif 3948  cun 3949
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-dif 3954  df-un 3956  df-vd1 44590
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator