Proof of Theorem disjdifprg
Step | Hyp | Ref
| Expression |
1 | | disjxsn 4646 |
. . . . . 6
⊢
Disj 𝑥 ∈
{∅}𝑥 |
2 | | simpr 477 |
. . . . . . . 8
⊢ ((𝐵 ∈ 𝑊 ∧ 𝐵 = ∅) → 𝐵 = ∅) |
3 | | eqidd 2623 |
. . . . . . . 8
⊢ ((𝐵 ∈ 𝑊 ∧ 𝐵 = ∅) → ∅ =
∅) |
4 | | elex 3212 |
. . . . . . . . . 10
⊢ (𝐵 ∈ 𝑊 → 𝐵 ∈ V) |
5 | | 0ex 4790 |
. . . . . . . . . . 11
⊢ ∅
∈ V |
6 | 5 | a1i 11 |
. . . . . . . . . 10
⊢ (𝐵 ∈ 𝑊 → ∅ ∈ V) |
7 | 4, 6, 6 | preqsnd 4392 |
. . . . . . . . 9
⊢ (𝐵 ∈ 𝑊 → ({𝐵, ∅} = {∅} ↔ (𝐵 = ∅ ∧ ∅ =
∅))) |
8 | 7 | adantr 481 |
. . . . . . . 8
⊢ ((𝐵 ∈ 𝑊 ∧ 𝐵 = ∅) → ({𝐵, ∅} = {∅} ↔ (𝐵 = ∅ ∧ ∅ =
∅))) |
9 | 2, 3, 8 | mpbir2and 957 |
. . . . . . 7
⊢ ((𝐵 ∈ 𝑊 ∧ 𝐵 = ∅) → {𝐵, ∅} = {∅}) |
10 | 9 | disjeq1d 4628 |
. . . . . 6
⊢ ((𝐵 ∈ 𝑊 ∧ 𝐵 = ∅) → (Disj 𝑥 ∈ {𝐵, ∅}𝑥 ↔ Disj 𝑥 ∈ {∅}𝑥)) |
11 | 1, 10 | mpbiri 248 |
. . . . 5
⊢ ((𝐵 ∈ 𝑊 ∧ 𝐵 = ∅) → Disj 𝑥 ∈ {𝐵, ∅}𝑥) |
12 | | in0 3968 |
. . . . . 6
⊢ (𝐵 ∩ ∅) =
∅ |
13 | 4 | adantr 481 |
. . . . . . 7
⊢ ((𝐵 ∈ 𝑊 ∧ 𝐵 ≠ ∅) → 𝐵 ∈ V) |
14 | 5 | a1i 11 |
. . . . . . 7
⊢ ((𝐵 ∈ 𝑊 ∧ 𝐵 ≠ ∅) → ∅ ∈
V) |
15 | | simpr 477 |
. . . . . . 7
⊢ ((𝐵 ∈ 𝑊 ∧ 𝐵 ≠ ∅) → 𝐵 ≠ ∅) |
16 | | id 22 |
. . . . . . . 8
⊢ (𝑥 = 𝐵 → 𝑥 = 𝐵) |
17 | | id 22 |
. . . . . . . 8
⊢ (𝑥 = ∅ → 𝑥 = ∅) |
18 | 16, 17 | disjprg 4648 |
. . . . . . 7
⊢ ((𝐵 ∈ V ∧ ∅ ∈ V
∧ 𝐵 ≠ ∅)
→ (Disj 𝑥
∈ {𝐵, ∅}𝑥 ↔ (𝐵 ∩ ∅) = ∅)) |
19 | 13, 14, 15, 18 | syl3anc 1326 |
. . . . . 6
⊢ ((𝐵 ∈ 𝑊 ∧ 𝐵 ≠ ∅) → (Disj 𝑥 ∈ {𝐵, ∅}𝑥 ↔ (𝐵 ∩ ∅) = ∅)) |
20 | 12, 19 | mpbiri 248 |
. . . . 5
⊢ ((𝐵 ∈ 𝑊 ∧ 𝐵 ≠ ∅) → Disj 𝑥 ∈ {𝐵, ∅}𝑥) |
21 | 11, 20 | pm2.61dane 2881 |
. . . 4
⊢ (𝐵 ∈ 𝑊 → Disj 𝑥 ∈ {𝐵, ∅}𝑥) |
22 | 21 | ad2antlr 763 |
. . 3
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ 𝐴 = ∅) → Disj 𝑥 ∈ {𝐵, ∅}𝑥) |
23 | | difeq2 3722 |
. . . . . . 7
⊢ (𝐴 = ∅ → (𝐵 ∖ 𝐴) = (𝐵 ∖ ∅)) |
24 | | dif0 3950 |
. . . . . . 7
⊢ (𝐵 ∖ ∅) = 𝐵 |
25 | 23, 24 | syl6eq 2672 |
. . . . . 6
⊢ (𝐴 = ∅ → (𝐵 ∖ 𝐴) = 𝐵) |
26 | | id 22 |
. . . . . 6
⊢ (𝐴 = ∅ → 𝐴 = ∅) |
27 | 25, 26 | preq12d 4276 |
. . . . 5
⊢ (𝐴 = ∅ → {(𝐵 ∖ 𝐴), 𝐴} = {𝐵, ∅}) |
28 | 27 | disjeq1d 4628 |
. . . 4
⊢ (𝐴 = ∅ → (Disj
𝑥 ∈ {(𝐵 ∖ 𝐴), 𝐴}𝑥 ↔ Disj 𝑥 ∈ {𝐵, ∅}𝑥)) |
29 | 28 | adantl 482 |
. . 3
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ 𝐴 = ∅) → (Disj 𝑥 ∈ {(𝐵 ∖ 𝐴), 𝐴}𝑥 ↔ Disj 𝑥 ∈ {𝐵, ∅}𝑥)) |
30 | 22, 29 | mpbird 247 |
. 2
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ 𝐴 = ∅) → Disj 𝑥 ∈ {(𝐵 ∖ 𝐴), 𝐴}𝑥) |
31 | | incom 3805 |
. . . 4
⊢ (𝐴 ∩ (𝐵 ∖ 𝐴)) = ((𝐵 ∖ 𝐴) ∩ 𝐴) |
32 | | disjdif 4040 |
. . . 4
⊢ (𝐴 ∩ (𝐵 ∖ 𝐴)) = ∅ |
33 | 31, 32 | eqtr3i 2646 |
. . 3
⊢ ((𝐵 ∖ 𝐴) ∩ 𝐴) = ∅ |
34 | | difexg 4808 |
. . . . 5
⊢ (𝐵 ∈ 𝑊 → (𝐵 ∖ 𝐴) ∈ V) |
35 | 34 | ad2antlr 763 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ ¬ 𝐴 = ∅) → (𝐵 ∖ 𝐴) ∈ V) |
36 | | elex 3212 |
. . . . 5
⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V) |
37 | 36 | ad2antrr 762 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ ¬ 𝐴 = ∅) → 𝐴 ∈ V) |
38 | | ssid 3624 |
. . . . . 6
⊢ (𝐵 ∖ 𝐴) ⊆ (𝐵 ∖ 𝐴) |
39 | | ssdifeq0 4051 |
. . . . . . . 8
⊢ (𝐴 ⊆ (𝐵 ∖ 𝐴) ↔ 𝐴 = ∅) |
40 | 39 | notbii 310 |
. . . . . . 7
⊢ (¬
𝐴 ⊆ (𝐵 ∖ 𝐴) ↔ ¬ 𝐴 = ∅) |
41 | | nssne2 3662 |
. . . . . . 7
⊢ (((𝐵 ∖ 𝐴) ⊆ (𝐵 ∖ 𝐴) ∧ ¬ 𝐴 ⊆ (𝐵 ∖ 𝐴)) → (𝐵 ∖ 𝐴) ≠ 𝐴) |
42 | 40, 41 | sylan2br 493 |
. . . . . 6
⊢ (((𝐵 ∖ 𝐴) ⊆ (𝐵 ∖ 𝐴) ∧ ¬ 𝐴 = ∅) → (𝐵 ∖ 𝐴) ≠ 𝐴) |
43 | 38, 42 | mpan 706 |
. . . . 5
⊢ (¬
𝐴 = ∅ → (𝐵 ∖ 𝐴) ≠ 𝐴) |
44 | 43 | adantl 482 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ ¬ 𝐴 = ∅) → (𝐵 ∖ 𝐴) ≠ 𝐴) |
45 | | id 22 |
. . . . 5
⊢ (𝑥 = (𝐵 ∖ 𝐴) → 𝑥 = (𝐵 ∖ 𝐴)) |
46 | | id 22 |
. . . . 5
⊢ (𝑥 = 𝐴 → 𝑥 = 𝐴) |
47 | 45, 46 | disjprg 4648 |
. . . 4
⊢ (((𝐵 ∖ 𝐴) ∈ V ∧ 𝐴 ∈ V ∧ (𝐵 ∖ 𝐴) ≠ 𝐴) → (Disj 𝑥 ∈ {(𝐵 ∖ 𝐴), 𝐴}𝑥 ↔ ((𝐵 ∖ 𝐴) ∩ 𝐴) = ∅)) |
48 | 35, 37, 44, 47 | syl3anc 1326 |
. . 3
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ ¬ 𝐴 = ∅) → (Disj 𝑥 ∈ {(𝐵 ∖ 𝐴), 𝐴}𝑥 ↔ ((𝐵 ∖ 𝐴) ∩ 𝐴) = ∅)) |
49 | 33, 48 | mpbiri 248 |
. 2
⊢ (((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) ∧ ¬ 𝐴 = ∅) → Disj 𝑥 ∈ {(𝐵 ∖ 𝐴), 𝐴}𝑥) |
50 | 30, 49 | pm2.61dan 832 |
1
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → Disj 𝑥 ∈ {(𝐵 ∖ 𝐴), 𝐴}𝑥) |