Step | Hyp | Ref
| Expression |
1 | | eliun 4460 |
. . . . . . . . . 10
⊢ (𝑠 ∈ ∪ 𝑐 ∈ (𝑊 ∖ {𝑎}){〈𝑎, 𝐵, 𝑐〉} ↔ ∃𝑐 ∈ (𝑊 ∖ {𝑎})𝑠 ∈ {〈𝑎, 𝐵, 𝑐〉}) |
2 | | otthg 4880 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑎 ∈ 𝑉 ∧ 𝐵 ∈ 𝑋 ∧ 𝑐 ∈ (𝑊 ∖ {𝑎})) → (〈𝑎, 𝐵, 𝑐〉 = 〈𝑑, 𝐵, 𝑒〉 ↔ (𝑎 = 𝑑 ∧ 𝐵 = 𝐵 ∧ 𝑐 = 𝑒))) |
3 | | simp1 1054 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑎 = 𝑑 ∧ 𝐵 = 𝐵 ∧ 𝑐 = 𝑒) → 𝑎 = 𝑑) |
4 | 2, 3 | syl6bi 242 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑎 ∈ 𝑉 ∧ 𝐵 ∈ 𝑋 ∧ 𝑐 ∈ (𝑊 ∖ {𝑎})) → (〈𝑎, 𝐵, 𝑐〉 = 〈𝑑, 𝐵, 𝑒〉 → 𝑎 = 𝑑)) |
5 | 4 | con3d 147 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑎 ∈ 𝑉 ∧ 𝐵 ∈ 𝑋 ∧ 𝑐 ∈ (𝑊 ∖ {𝑎})) → (¬ 𝑎 = 𝑑 → ¬ 〈𝑎, 𝐵, 𝑐〉 = 〈𝑑, 𝐵, 𝑒〉)) |
6 | 5 | 3exp 1256 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑎 ∈ 𝑉 → (𝐵 ∈ 𝑋 → (𝑐 ∈ (𝑊 ∖ {𝑎}) → (¬ 𝑎 = 𝑑 → ¬ 〈𝑎, 𝐵, 𝑐〉 = 〈𝑑, 𝐵, 𝑒〉)))) |
7 | 6 | impcom 445 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐵 ∈ 𝑋 ∧ 𝑎 ∈ 𝑉) → (𝑐 ∈ (𝑊 ∖ {𝑎}) → (¬ 𝑎 = 𝑑 → ¬ 〈𝑎, 𝐵, 𝑐〉 = 〈𝑑, 𝐵, 𝑒〉))) |
8 | 7 | com3r 85 |
. . . . . . . . . . . . . . . . . . 19
⊢ (¬
𝑎 = 𝑑 → ((𝐵 ∈ 𝑋 ∧ 𝑎 ∈ 𝑉) → (𝑐 ∈ (𝑊 ∖ {𝑎}) → ¬ 〈𝑎, 𝐵, 𝑐〉 = 〈𝑑, 𝐵, 𝑒〉))) |
9 | 8 | imp31 447 |
. . . . . . . . . . . . . . . . . 18
⊢ (((¬
𝑎 = 𝑑 ∧ (𝐵 ∈ 𝑋 ∧ 𝑎 ∈ 𝑉)) ∧ 𝑐 ∈ (𝑊 ∖ {𝑎})) → ¬ 〈𝑎, 𝐵, 𝑐〉 = 〈𝑑, 𝐵, 𝑒〉) |
10 | | velsn 4141 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑠 ∈ {〈𝑎, 𝐵, 𝑐〉} ↔ 𝑠 = 〈𝑎, 𝐵, 𝑐〉) |
11 | | eqeq1 2614 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑠 = 〈𝑎, 𝐵, 𝑐〉 → (𝑠 = 〈𝑑, 𝐵, 𝑒〉 ↔ 〈𝑎, 𝐵, 𝑐〉 = 〈𝑑, 𝐵, 𝑒〉)) |
12 | 11 | notbid 307 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑠 = 〈𝑎, 𝐵, 𝑐〉 → (¬ 𝑠 = 〈𝑑, 𝐵, 𝑒〉 ↔ ¬ 〈𝑎, 𝐵, 𝑐〉 = 〈𝑑, 𝐵, 𝑒〉)) |
13 | 10, 12 | sylbi 206 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑠 ∈ {〈𝑎, 𝐵, 𝑐〉} → (¬ 𝑠 = 〈𝑑, 𝐵, 𝑒〉 ↔ ¬ 〈𝑎, 𝐵, 𝑐〉 = 〈𝑑, 𝐵, 𝑒〉)) |
14 | 9, 13 | syl5ibrcom 236 |
. . . . . . . . . . . . . . . . 17
⊢ (((¬
𝑎 = 𝑑 ∧ (𝐵 ∈ 𝑋 ∧ 𝑎 ∈ 𝑉)) ∧ 𝑐 ∈ (𝑊 ∖ {𝑎})) → (𝑠 ∈ {〈𝑎, 𝐵, 𝑐〉} → ¬ 𝑠 = 〈𝑑, 𝐵, 𝑒〉)) |
15 | 14 | imp 444 |
. . . . . . . . . . . . . . . 16
⊢ ((((¬
𝑎 = 𝑑 ∧ (𝐵 ∈ 𝑋 ∧ 𝑎 ∈ 𝑉)) ∧ 𝑐 ∈ (𝑊 ∖ {𝑎})) ∧ 𝑠 ∈ {〈𝑎, 𝐵, 𝑐〉}) → ¬ 𝑠 = 〈𝑑, 𝐵, 𝑒〉) |
16 | | velsn 4141 |
. . . . . . . . . . . . . . . 16
⊢ (𝑠 ∈ {〈𝑑, 𝐵, 𝑒〉} ↔ 𝑠 = 〈𝑑, 𝐵, 𝑒〉) |
17 | 15, 16 | sylnibr 318 |
. . . . . . . . . . . . . . 15
⊢ ((((¬
𝑎 = 𝑑 ∧ (𝐵 ∈ 𝑋 ∧ 𝑎 ∈ 𝑉)) ∧ 𝑐 ∈ (𝑊 ∖ {𝑎})) ∧ 𝑠 ∈ {〈𝑎, 𝐵, 𝑐〉}) → ¬ 𝑠 ∈ {〈𝑑, 𝐵, 𝑒〉}) |
18 | 17 | adantr 480 |
. . . . . . . . . . . . . 14
⊢
(((((¬ 𝑎 = 𝑑 ∧ (𝐵 ∈ 𝑋 ∧ 𝑎 ∈ 𝑉)) ∧ 𝑐 ∈ (𝑊 ∖ {𝑎})) ∧ 𝑠 ∈ {〈𝑎, 𝐵, 𝑐〉}) ∧ 𝑒 ∈ (𝑊 ∖ {𝑑})) → ¬ 𝑠 ∈ {〈𝑑, 𝐵, 𝑒〉}) |
19 | 18 | nrexdv 2984 |
. . . . . . . . . . . . 13
⊢ ((((¬
𝑎 = 𝑑 ∧ (𝐵 ∈ 𝑋 ∧ 𝑎 ∈ 𝑉)) ∧ 𝑐 ∈ (𝑊 ∖ {𝑎})) ∧ 𝑠 ∈ {〈𝑎, 𝐵, 𝑐〉}) → ¬ ∃𝑒 ∈ (𝑊 ∖ {𝑑})𝑠 ∈ {〈𝑑, 𝐵, 𝑒〉}) |
20 | | eliun 4460 |
. . . . . . . . . . . . 13
⊢ (𝑠 ∈ ∪ 𝑒 ∈ (𝑊 ∖ {𝑑}){〈𝑑, 𝐵, 𝑒〉} ↔ ∃𝑒 ∈ (𝑊 ∖ {𝑑})𝑠 ∈ {〈𝑑, 𝐵, 𝑒〉}) |
21 | 19, 20 | sylnibr 318 |
. . . . . . . . . . . 12
⊢ ((((¬
𝑎 = 𝑑 ∧ (𝐵 ∈ 𝑋 ∧ 𝑎 ∈ 𝑉)) ∧ 𝑐 ∈ (𝑊 ∖ {𝑎})) ∧ 𝑠 ∈ {〈𝑎, 𝐵, 𝑐〉}) → ¬ 𝑠 ∈ ∪
𝑒 ∈ (𝑊 ∖ {𝑑}){〈𝑑, 𝐵, 𝑒〉}) |
22 | 21 | ex 449 |
. . . . . . . . . . 11
⊢ (((¬
𝑎 = 𝑑 ∧ (𝐵 ∈ 𝑋 ∧ 𝑎 ∈ 𝑉)) ∧ 𝑐 ∈ (𝑊 ∖ {𝑎})) → (𝑠 ∈ {〈𝑎, 𝐵, 𝑐〉} → ¬ 𝑠 ∈ ∪
𝑒 ∈ (𝑊 ∖ {𝑑}){〈𝑑, 𝐵, 𝑒〉})) |
23 | 22 | rexlimdva 3013 |
. . . . . . . . . 10
⊢ ((¬
𝑎 = 𝑑 ∧ (𝐵 ∈ 𝑋 ∧ 𝑎 ∈ 𝑉)) → (∃𝑐 ∈ (𝑊 ∖ {𝑎})𝑠 ∈ {〈𝑎, 𝐵, 𝑐〉} → ¬ 𝑠 ∈ ∪
𝑒 ∈ (𝑊 ∖ {𝑑}){〈𝑑, 𝐵, 𝑒〉})) |
24 | 1, 23 | syl5bi 231 |
. . . . . . . . 9
⊢ ((¬
𝑎 = 𝑑 ∧ (𝐵 ∈ 𝑋 ∧ 𝑎 ∈ 𝑉)) → (𝑠 ∈ ∪
𝑐 ∈ (𝑊 ∖ {𝑎}){〈𝑎, 𝐵, 𝑐〉} → ¬ 𝑠 ∈ ∪
𝑒 ∈ (𝑊 ∖ {𝑑}){〈𝑑, 𝐵, 𝑒〉})) |
25 | 24 | ralrimiv 2948 |
. . . . . . . 8
⊢ ((¬
𝑎 = 𝑑 ∧ (𝐵 ∈ 𝑋 ∧ 𝑎 ∈ 𝑉)) → ∀𝑠 ∈ ∪
𝑐 ∈ (𝑊 ∖ {𝑎}){〈𝑎, 𝐵, 𝑐〉} ¬ 𝑠 ∈ ∪
𝑒 ∈ (𝑊 ∖ {𝑑}){〈𝑑, 𝐵, 𝑒〉}) |
26 | | oteq3 4351 |
. . . . . . . . . . . . 13
⊢ (𝑐 = 𝑒 → 〈𝑑, 𝐵, 𝑐〉 = 〈𝑑, 𝐵, 𝑒〉) |
27 | 26 | sneqd 4137 |
. . . . . . . . . . . 12
⊢ (𝑐 = 𝑒 → {〈𝑑, 𝐵, 𝑐〉} = {〈𝑑, 𝐵, 𝑒〉}) |
28 | 27 | cbviunv 4495 |
. . . . . . . . . . 11
⊢ ∪ 𝑐 ∈ (𝑊 ∖ {𝑑}){〈𝑑, 𝐵, 𝑐〉} = ∪
𝑒 ∈ (𝑊 ∖ {𝑑}){〈𝑑, 𝐵, 𝑒〉} |
29 | 28 | eleq2i 2680 |
. . . . . . . . . 10
⊢ (𝑠 ∈ ∪ 𝑐 ∈ (𝑊 ∖ {𝑑}){〈𝑑, 𝐵, 𝑐〉} ↔ 𝑠 ∈ ∪
𝑒 ∈ (𝑊 ∖ {𝑑}){〈𝑑, 𝐵, 𝑒〉}) |
30 | 29 | notbii 309 |
. . . . . . . . 9
⊢ (¬
𝑠 ∈ ∪ 𝑐 ∈ (𝑊 ∖ {𝑑}){〈𝑑, 𝐵, 𝑐〉} ↔ ¬ 𝑠 ∈ ∪
𝑒 ∈ (𝑊 ∖ {𝑑}){〈𝑑, 𝐵, 𝑒〉}) |
31 | 30 | ralbii 2963 |
. . . . . . . 8
⊢
(∀𝑠 ∈
∪ 𝑐 ∈ (𝑊 ∖ {𝑎}){〈𝑎, 𝐵, 𝑐〉} ¬ 𝑠 ∈ ∪
𝑐 ∈ (𝑊 ∖ {𝑑}){〈𝑑, 𝐵, 𝑐〉} ↔ ∀𝑠 ∈ ∪
𝑐 ∈ (𝑊 ∖ {𝑎}){〈𝑎, 𝐵, 𝑐〉} ¬ 𝑠 ∈ ∪
𝑒 ∈ (𝑊 ∖ {𝑑}){〈𝑑, 𝐵, 𝑒〉}) |
32 | 25, 31 | sylibr 223 |
. . . . . . 7
⊢ ((¬
𝑎 = 𝑑 ∧ (𝐵 ∈ 𝑋 ∧ 𝑎 ∈ 𝑉)) → ∀𝑠 ∈ ∪
𝑐 ∈ (𝑊 ∖ {𝑎}){〈𝑎, 𝐵, 𝑐〉} ¬ 𝑠 ∈ ∪
𝑐 ∈ (𝑊 ∖ {𝑑}){〈𝑑, 𝐵, 𝑐〉}) |
33 | | disj 3969 |
. . . . . . 7
⊢
((∪ 𝑐 ∈ (𝑊 ∖ {𝑎}){〈𝑎, 𝐵, 𝑐〉} ∩ ∪ 𝑐 ∈ (𝑊 ∖ {𝑑}){〈𝑑, 𝐵, 𝑐〉}) = ∅ ↔ ∀𝑠 ∈ ∪ 𝑐 ∈ (𝑊 ∖ {𝑎}){〈𝑎, 𝐵, 𝑐〉} ¬ 𝑠 ∈ ∪
𝑐 ∈ (𝑊 ∖ {𝑑}){〈𝑑, 𝐵, 𝑐〉}) |
34 | 32, 33 | sylibr 223 |
. . . . . 6
⊢ ((¬
𝑎 = 𝑑 ∧ (𝐵 ∈ 𝑋 ∧ 𝑎 ∈ 𝑉)) → (∪ 𝑐 ∈ (𝑊 ∖ {𝑎}){〈𝑎, 𝐵, 𝑐〉} ∩ ∪ 𝑐 ∈ (𝑊 ∖ {𝑑}){〈𝑑, 𝐵, 𝑐〉}) = ∅) |
35 | 34 | expcom 450 |
. . . . 5
⊢ ((𝐵 ∈ 𝑋 ∧ 𝑎 ∈ 𝑉) → (¬ 𝑎 = 𝑑 → (∪
𝑐 ∈ (𝑊 ∖ {𝑎}){〈𝑎, 𝐵, 𝑐〉} ∩ ∪ 𝑐 ∈ (𝑊 ∖ {𝑑}){〈𝑑, 𝐵, 𝑐〉}) = ∅)) |
36 | 35 | orrd 392 |
. . . 4
⊢ ((𝐵 ∈ 𝑋 ∧ 𝑎 ∈ 𝑉) → (𝑎 = 𝑑 ∨ (∪
𝑐 ∈ (𝑊 ∖ {𝑎}){〈𝑎, 𝐵, 𝑐〉} ∩ ∪ 𝑐 ∈ (𝑊 ∖ {𝑑}){〈𝑑, 𝐵, 𝑐〉}) = ∅)) |
37 | 36 | adantrr 749 |
. . 3
⊢ ((𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉)) → (𝑎 = 𝑑 ∨ (∪
𝑐 ∈ (𝑊 ∖ {𝑎}){〈𝑎, 𝐵, 𝑐〉} ∩ ∪ 𝑐 ∈ (𝑊 ∖ {𝑑}){〈𝑑, 𝐵, 𝑐〉}) = ∅)) |
38 | 37 | ralrimivva 2954 |
. 2
⊢ (𝐵 ∈ 𝑋 → ∀𝑎 ∈ 𝑉 ∀𝑑 ∈ 𝑉 (𝑎 = 𝑑 ∨ (∪
𝑐 ∈ (𝑊 ∖ {𝑎}){〈𝑎, 𝐵, 𝑐〉} ∩ ∪ 𝑐 ∈ (𝑊 ∖ {𝑑}){〈𝑑, 𝐵, 𝑐〉}) = ∅)) |
39 | | sneq 4135 |
. . . . 5
⊢ (𝑎 = 𝑑 → {𝑎} = {𝑑}) |
40 | 39 | difeq2d 3690 |
. . . 4
⊢ (𝑎 = 𝑑 → (𝑊 ∖ {𝑎}) = (𝑊 ∖ {𝑑})) |
41 | | oteq1 4349 |
. . . . 5
⊢ (𝑎 = 𝑑 → 〈𝑎, 𝐵, 𝑐〉 = 〈𝑑, 𝐵, 𝑐〉) |
42 | 41 | sneqd 4137 |
. . . 4
⊢ (𝑎 = 𝑑 → {〈𝑎, 𝐵, 𝑐〉} = {〈𝑑, 𝐵, 𝑐〉}) |
43 | 40, 42 | iuneq12d 4482 |
. . 3
⊢ (𝑎 = 𝑑 → ∪
𝑐 ∈ (𝑊 ∖ {𝑎}){〈𝑎, 𝐵, 𝑐〉} = ∪
𝑐 ∈ (𝑊 ∖ {𝑑}){〈𝑑, 𝐵, 𝑐〉}) |
44 | 43 | disjor 4567 |
. 2
⊢
(Disj 𝑎
∈ 𝑉 ∪ 𝑐 ∈ (𝑊 ∖ {𝑎}){〈𝑎, 𝐵, 𝑐〉} ↔ ∀𝑎 ∈ 𝑉 ∀𝑑 ∈ 𝑉 (𝑎 = 𝑑 ∨ (∪
𝑐 ∈ (𝑊 ∖ {𝑎}){〈𝑎, 𝐵, 𝑐〉} ∩ ∪ 𝑐 ∈ (𝑊 ∖ {𝑑}){〈𝑑, 𝐵, 𝑐〉}) = ∅)) |
45 | 38, 44 | sylibr 223 |
1
⊢ (𝐵 ∈ 𝑋 → Disj 𝑎 ∈ 𝑉 ∪ 𝑐 ∈ (𝑊 ∖ {𝑎}){〈𝑎, 𝐵, 𝑐〉}) |