Step | Hyp | Ref
| Expression |
1 | | eqeq1 2743 |
. . . . . . 7
⊢ (𝑦 = 𝐴 → (𝑦 = 𝑧 ↔ 𝐴 = 𝑧)) |
2 | | nfcv 2900 |
. . . . . . . . . 10
⊢
Ⅎ𝑥𝐴 |
3 | | nfcv 2900 |
. . . . . . . . . 10
⊢
Ⅎ𝑥𝐷 |
4 | | disjprgw.1 |
. . . . . . . . . 10
⊢ (𝑥 = 𝐴 → 𝐶 = 𝐷) |
5 | 2, 3, 4 | csbhypf 3819 |
. . . . . . . . 9
⊢ (𝑦 = 𝐴 → ⦋𝑦 / 𝑥⦌𝐶 = 𝐷) |
6 | 5 | ineq1d 4103 |
. . . . . . . 8
⊢ (𝑦 = 𝐴 → (⦋𝑦 / 𝑥⦌𝐶 ∩ ⦋𝑧 / 𝑥⦌𝐶) = (𝐷 ∩ ⦋𝑧 / 𝑥⦌𝐶)) |
7 | 6 | eqeq1d 2741 |
. . . . . . 7
⊢ (𝑦 = 𝐴 → ((⦋𝑦 / 𝑥⦌𝐶 ∩ ⦋𝑧 / 𝑥⦌𝐶) = ∅ ↔ (𝐷 ∩ ⦋𝑧 / 𝑥⦌𝐶) = ∅)) |
8 | 1, 7 | orbi12d 918 |
. . . . . 6
⊢ (𝑦 = 𝐴 → ((𝑦 = 𝑧 ∨ (⦋𝑦 / 𝑥⦌𝐶 ∩ ⦋𝑧 / 𝑥⦌𝐶) = ∅) ↔ (𝐴 = 𝑧 ∨ (𝐷 ∩ ⦋𝑧 / 𝑥⦌𝐶) = ∅))) |
9 | 8 | ralbidv 3110 |
. . . . 5
⊢ (𝑦 = 𝐴 → (∀𝑧 ∈ {𝐴, 𝐵} (𝑦 = 𝑧 ∨ (⦋𝑦 / 𝑥⦌𝐶 ∩ ⦋𝑧 / 𝑥⦌𝐶) = ∅) ↔ ∀𝑧 ∈ {𝐴, 𝐵} (𝐴 = 𝑧 ∨ (𝐷 ∩ ⦋𝑧 / 𝑥⦌𝐶) = ∅))) |
10 | | eqeq1 2743 |
. . . . . . 7
⊢ (𝑦 = 𝐵 → (𝑦 = 𝑧 ↔ 𝐵 = 𝑧)) |
11 | | nfcv 2900 |
. . . . . . . . . 10
⊢
Ⅎ𝑥𝐵 |
12 | | nfcv 2900 |
. . . . . . . . . 10
⊢
Ⅎ𝑥𝐸 |
13 | | disjprgw.2 |
. . . . . . . . . 10
⊢ (𝑥 = 𝐵 → 𝐶 = 𝐸) |
14 | 11, 12, 13 | csbhypf 3819 |
. . . . . . . . 9
⊢ (𝑦 = 𝐵 → ⦋𝑦 / 𝑥⦌𝐶 = 𝐸) |
15 | 14 | ineq1d 4103 |
. . . . . . . 8
⊢ (𝑦 = 𝐵 → (⦋𝑦 / 𝑥⦌𝐶 ∩ ⦋𝑧 / 𝑥⦌𝐶) = (𝐸 ∩ ⦋𝑧 / 𝑥⦌𝐶)) |
16 | 15 | eqeq1d 2741 |
. . . . . . 7
⊢ (𝑦 = 𝐵 → ((⦋𝑦 / 𝑥⦌𝐶 ∩ ⦋𝑧 / 𝑥⦌𝐶) = ∅ ↔ (𝐸 ∩ ⦋𝑧 / 𝑥⦌𝐶) = ∅)) |
17 | 10, 16 | orbi12d 918 |
. . . . . 6
⊢ (𝑦 = 𝐵 → ((𝑦 = 𝑧 ∨ (⦋𝑦 / 𝑥⦌𝐶 ∩ ⦋𝑧 / 𝑥⦌𝐶) = ∅) ↔ (𝐵 = 𝑧 ∨ (𝐸 ∩ ⦋𝑧 / 𝑥⦌𝐶) = ∅))) |
18 | 17 | ralbidv 3110 |
. . . . 5
⊢ (𝑦 = 𝐵 → (∀𝑧 ∈ {𝐴, 𝐵} (𝑦 = 𝑧 ∨ (⦋𝑦 / 𝑥⦌𝐶 ∩ ⦋𝑧 / 𝑥⦌𝐶) = ∅) ↔ ∀𝑧 ∈ {𝐴, 𝐵} (𝐵 = 𝑧 ∨ (𝐸 ∩ ⦋𝑧 / 𝑥⦌𝐶) = ∅))) |
19 | 9, 18 | ralprg 4586 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (∀𝑦 ∈ {𝐴, 𝐵}∀𝑧 ∈ {𝐴, 𝐵} (𝑦 = 𝑧 ∨ (⦋𝑦 / 𝑥⦌𝐶 ∩ ⦋𝑧 / 𝑥⦌𝐶) = ∅) ↔ (∀𝑧 ∈ {𝐴, 𝐵} (𝐴 = 𝑧 ∨ (𝐷 ∩ ⦋𝑧 / 𝑥⦌𝐶) = ∅) ∧ ∀𝑧 ∈ {𝐴, 𝐵} (𝐵 = 𝑧 ∨ (𝐸 ∩ ⦋𝑧 / 𝑥⦌𝐶) = ∅)))) |
20 | 19 | 3adant3 1133 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵) → (∀𝑦 ∈ {𝐴, 𝐵}∀𝑧 ∈ {𝐴, 𝐵} (𝑦 = 𝑧 ∨ (⦋𝑦 / 𝑥⦌𝐶 ∩ ⦋𝑧 / 𝑥⦌𝐶) = ∅) ↔ (∀𝑧 ∈ {𝐴, 𝐵} (𝐴 = 𝑧 ∨ (𝐷 ∩ ⦋𝑧 / 𝑥⦌𝐶) = ∅) ∧ ∀𝑧 ∈ {𝐴, 𝐵} (𝐵 = 𝑧 ∨ (𝐸 ∩ ⦋𝑧 / 𝑥⦌𝐶) = ∅)))) |
21 | | id 22 |
. . . . . . . . . 10
⊢ (𝑧 = 𝐴 → 𝑧 = 𝐴) |
22 | 21 | eqcomd 2745 |
. . . . . . . . 9
⊢ (𝑧 = 𝐴 → 𝐴 = 𝑧) |
23 | 22 | orcd 872 |
. . . . . . . 8
⊢ (𝑧 = 𝐴 → (𝐴 = 𝑧 ∨ (𝐷 ∩ ⦋𝑧 / 𝑥⦌𝐶) = ∅)) |
24 | | trud 1552 |
. . . . . . . 8
⊢ (𝑧 = 𝐴 → ⊤) |
25 | 23, 24 | 2thd 268 |
. . . . . . 7
⊢ (𝑧 = 𝐴 → ((𝐴 = 𝑧 ∨ (𝐷 ∩ ⦋𝑧 / 𝑥⦌𝐶) = ∅) ↔
⊤)) |
26 | | eqeq2 2751 |
. . . . . . . 8
⊢ (𝑧 = 𝐵 → (𝐴 = 𝑧 ↔ 𝐴 = 𝐵)) |
27 | 11, 12, 13 | csbhypf 3819 |
. . . . . . . . . 10
⊢ (𝑧 = 𝐵 → ⦋𝑧 / 𝑥⦌𝐶 = 𝐸) |
28 | 27 | ineq2d 4104 |
. . . . . . . . 9
⊢ (𝑧 = 𝐵 → (𝐷 ∩ ⦋𝑧 / 𝑥⦌𝐶) = (𝐷 ∩ 𝐸)) |
29 | 28 | eqeq1d 2741 |
. . . . . . . 8
⊢ (𝑧 = 𝐵 → ((𝐷 ∩ ⦋𝑧 / 𝑥⦌𝐶) = ∅ ↔ (𝐷 ∩ 𝐸) = ∅)) |
30 | 26, 29 | orbi12d 918 |
. . . . . . 7
⊢ (𝑧 = 𝐵 → ((𝐴 = 𝑧 ∨ (𝐷 ∩ ⦋𝑧 / 𝑥⦌𝐶) = ∅) ↔ (𝐴 = 𝐵 ∨ (𝐷 ∩ 𝐸) = ∅))) |
31 | 25, 30 | ralprg 4586 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (∀𝑧 ∈ {𝐴, 𝐵} (𝐴 = 𝑧 ∨ (𝐷 ∩ ⦋𝑧 / 𝑥⦌𝐶) = ∅) ↔ (⊤ ∧ (𝐴 = 𝐵 ∨ (𝐷 ∩ 𝐸) = ∅)))) |
32 | 31 | 3adant3 1133 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵) → (∀𝑧 ∈ {𝐴, 𝐵} (𝐴 = 𝑧 ∨ (𝐷 ∩ ⦋𝑧 / 𝑥⦌𝐶) = ∅) ↔ (⊤ ∧ (𝐴 = 𝐵 ∨ (𝐷 ∩ 𝐸) = ∅)))) |
33 | | simp3 1139 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵) → 𝐴 ≠ 𝐵) |
34 | | neneq 2941 |
. . . . . . 7
⊢ (𝐴 ≠ 𝐵 → ¬ 𝐴 = 𝐵) |
35 | | biorf 936 |
. . . . . . 7
⊢ (¬
𝐴 = 𝐵 → ((𝐷 ∩ 𝐸) = ∅ ↔ (𝐴 = 𝐵 ∨ (𝐷 ∩ 𝐸) = ∅))) |
36 | 33, 34, 35 | 3syl 18 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵) → ((𝐷 ∩ 𝐸) = ∅ ↔ (𝐴 = 𝐵 ∨ (𝐷 ∩ 𝐸) = ∅))) |
37 | | tru 1546 |
. . . . . . 7
⊢
⊤ |
38 | 37 | biantrur 534 |
. . . . . 6
⊢ ((𝐴 = 𝐵 ∨ (𝐷 ∩ 𝐸) = ∅) ↔ (⊤ ∧ (𝐴 = 𝐵 ∨ (𝐷 ∩ 𝐸) = ∅))) |
39 | 36, 38 | bitrdi 290 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵) → ((𝐷 ∩ 𝐸) = ∅ ↔ (⊤ ∧ (𝐴 = 𝐵 ∨ (𝐷 ∩ 𝐸) = ∅)))) |
40 | 32, 39 | bitr4d 285 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵) → (∀𝑧 ∈ {𝐴, 𝐵} (𝐴 = 𝑧 ∨ (𝐷 ∩ ⦋𝑧 / 𝑥⦌𝐶) = ∅) ↔ (𝐷 ∩ 𝐸) = ∅)) |
41 | | eqeq2 2751 |
. . . . . . . . 9
⊢ (𝑧 = 𝐴 → (𝐵 = 𝑧 ↔ 𝐵 = 𝐴)) |
42 | | eqcom 2746 |
. . . . . . . . 9
⊢ (𝐵 = 𝐴 ↔ 𝐴 = 𝐵) |
43 | 41, 42 | bitrdi 290 |
. . . . . . . 8
⊢ (𝑧 = 𝐴 → (𝐵 = 𝑧 ↔ 𝐴 = 𝐵)) |
44 | 2, 3, 4 | csbhypf 3819 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝐴 → ⦋𝑧 / 𝑥⦌𝐶 = 𝐷) |
45 | 44 | ineq2d 4104 |
. . . . . . . . . 10
⊢ (𝑧 = 𝐴 → (𝐸 ∩ ⦋𝑧 / 𝑥⦌𝐶) = (𝐸 ∩ 𝐷)) |
46 | | incom 4092 |
. . . . . . . . . 10
⊢ (𝐸 ∩ 𝐷) = (𝐷 ∩ 𝐸) |
47 | 45, 46 | eqtrdi 2790 |
. . . . . . . . 9
⊢ (𝑧 = 𝐴 → (𝐸 ∩ ⦋𝑧 / 𝑥⦌𝐶) = (𝐷 ∩ 𝐸)) |
48 | 47 | eqeq1d 2741 |
. . . . . . . 8
⊢ (𝑧 = 𝐴 → ((𝐸 ∩ ⦋𝑧 / 𝑥⦌𝐶) = ∅ ↔ (𝐷 ∩ 𝐸) = ∅)) |
49 | 43, 48 | orbi12d 918 |
. . . . . . 7
⊢ (𝑧 = 𝐴 → ((𝐵 = 𝑧 ∨ (𝐸 ∩ ⦋𝑧 / 𝑥⦌𝐶) = ∅) ↔ (𝐴 = 𝐵 ∨ (𝐷 ∩ 𝐸) = ∅))) |
50 | | id 22 |
. . . . . . . . . 10
⊢ (𝑧 = 𝐵 → 𝑧 = 𝐵) |
51 | 50 | eqcomd 2745 |
. . . . . . . . 9
⊢ (𝑧 = 𝐵 → 𝐵 = 𝑧) |
52 | 51 | orcd 872 |
. . . . . . . 8
⊢ (𝑧 = 𝐵 → (𝐵 = 𝑧 ∨ (𝐸 ∩ ⦋𝑧 / 𝑥⦌𝐶) = ∅)) |
53 | | trud 1552 |
. . . . . . . 8
⊢ (𝑧 = 𝐵 → ⊤) |
54 | 52, 53 | 2thd 268 |
. . . . . . 7
⊢ (𝑧 = 𝐵 → ((𝐵 = 𝑧 ∨ (𝐸 ∩ ⦋𝑧 / 𝑥⦌𝐶) = ∅) ↔
⊤)) |
55 | 49, 54 | ralprg 4586 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (∀𝑧 ∈ {𝐴, 𝐵} (𝐵 = 𝑧 ∨ (𝐸 ∩ ⦋𝑧 / 𝑥⦌𝐶) = ∅) ↔ ((𝐴 = 𝐵 ∨ (𝐷 ∩ 𝐸) = ∅) ∧
⊤))) |
56 | 55 | 3adant3 1133 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵) → (∀𝑧 ∈ {𝐴, 𝐵} (𝐵 = 𝑧 ∨ (𝐸 ∩ ⦋𝑧 / 𝑥⦌𝐶) = ∅) ↔ ((𝐴 = 𝐵 ∨ (𝐷 ∩ 𝐸) = ∅) ∧
⊤))) |
57 | 37 | biantru 533 |
. . . . . 6
⊢ ((𝐴 = 𝐵 ∨ (𝐷 ∩ 𝐸) = ∅) ↔ ((𝐴 = 𝐵 ∨ (𝐷 ∩ 𝐸) = ∅) ∧
⊤)) |
58 | 36, 57 | bitrdi 290 |
. . . . 5
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵) → ((𝐷 ∩ 𝐸) = ∅ ↔ ((𝐴 = 𝐵 ∨ (𝐷 ∩ 𝐸) = ∅) ∧
⊤))) |
59 | 56, 58 | bitr4d 285 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵) → (∀𝑧 ∈ {𝐴, 𝐵} (𝐵 = 𝑧 ∨ (𝐸 ∩ ⦋𝑧 / 𝑥⦌𝐶) = ∅) ↔ (𝐷 ∩ 𝐸) = ∅)) |
60 | 40, 59 | anbi12d 634 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵) → ((∀𝑧 ∈ {𝐴, 𝐵} (𝐴 = 𝑧 ∨ (𝐷 ∩ ⦋𝑧 / 𝑥⦌𝐶) = ∅) ∧ ∀𝑧 ∈ {𝐴, 𝐵} (𝐵 = 𝑧 ∨ (𝐸 ∩ ⦋𝑧 / 𝑥⦌𝐶) = ∅)) ↔ ((𝐷 ∩ 𝐸) = ∅ ∧ (𝐷 ∩ 𝐸) = ∅))) |
61 | 20, 60 | bitrd 282 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵) → (∀𝑦 ∈ {𝐴, 𝐵}∀𝑧 ∈ {𝐴, 𝐵} (𝑦 = 𝑧 ∨ (⦋𝑦 / 𝑥⦌𝐶 ∩ ⦋𝑧 / 𝑥⦌𝐶) = ∅) ↔ ((𝐷 ∩ 𝐸) = ∅ ∧ (𝐷 ∩ 𝐸) = ∅))) |
62 | | disjors 5012 |
. 2
⊢
(Disj 𝑥
∈ {𝐴, 𝐵}𝐶 ↔ ∀𝑦 ∈ {𝐴, 𝐵}∀𝑧 ∈ {𝐴, 𝐵} (𝑦 = 𝑧 ∨ (⦋𝑦 / 𝑥⦌𝐶 ∩ ⦋𝑧 / 𝑥⦌𝐶) = ∅)) |
63 | | pm4.24 567 |
. 2
⊢ ((𝐷 ∩ 𝐸) = ∅ ↔ ((𝐷 ∩ 𝐸) = ∅ ∧ (𝐷 ∩ 𝐸) = ∅)) |
64 | 61, 62, 63 | 3bitr4g 317 |
1
⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐴 ≠ 𝐵) → (Disj 𝑥 ∈ {𝐴, 𝐵}𝐶 ↔ (𝐷 ∩ 𝐸) = ∅)) |