Step | Hyp | Ref
| Expression |
1 | | orc 866 |
. . . . 5
⊢ (𝑎 = 𝑑 → (𝑎 = 𝑑 ∨ (∪
𝑐 ∈ 𝑊 {〈𝑎, 𝐵, 𝑐〉} ∩ ∪ 𝑐 ∈ 𝑊 {〈𝑑, 𝐵, 𝑐〉}) = ∅)) |
2 | 1 | a1d 25 |
. . . 4
⊢ (𝑎 = 𝑑 → ((𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉)) → (𝑎 = 𝑑 ∨ (∪
𝑐 ∈ 𝑊 {〈𝑎, 𝐵, 𝑐〉} ∩ ∪ 𝑐 ∈ 𝑊 {〈𝑑, 𝐵, 𝑐〉}) = ∅))) |
3 | | eliun 4885 |
. . . . . . . . . 10
⊢ (𝑠 ∈ ∪ 𝑐 ∈ 𝑊 {〈𝑎, 𝐵, 𝑐〉} ↔ ∃𝑐 ∈ 𝑊 𝑠 ∈ {〈𝑎, 𝐵, 𝑐〉}) |
4 | | simprl 771 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉)) → 𝑎 ∈ 𝑉) |
5 | 4 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑐 ∈ 𝑊 ∧ (𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉))) → 𝑎 ∈ 𝑉) |
6 | | simprl 771 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑐 ∈ 𝑊 ∧ (𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉))) → 𝐵 ∈ 𝑋) |
7 | | simpl 486 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑐 ∈ 𝑊 ∧ (𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉))) → 𝑐 ∈ 𝑊) |
8 | | otthg 5343 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑎 ∈ 𝑉 ∧ 𝐵 ∈ 𝑋 ∧ 𝑐 ∈ 𝑊) → (〈𝑎, 𝐵, 𝑐〉 = 〈𝑑, 𝐵, 𝑒〉 ↔ (𝑎 = 𝑑 ∧ 𝐵 = 𝐵 ∧ 𝑐 = 𝑒))) |
9 | 5, 6, 7, 8 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑐 ∈ 𝑊 ∧ (𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉))) → (〈𝑎, 𝐵, 𝑐〉 = 〈𝑑, 𝐵, 𝑒〉 ↔ (𝑎 = 𝑑 ∧ 𝐵 = 𝐵 ∧ 𝑐 = 𝑒))) |
10 | | simp1 1137 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑎 = 𝑑 ∧ 𝐵 = 𝐵 ∧ 𝑐 = 𝑒) → 𝑎 = 𝑑) |
11 | 9, 10 | syl6bi 256 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑐 ∈ 𝑊 ∧ (𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉))) → (〈𝑎, 𝐵, 𝑐〉 = 〈𝑑, 𝐵, 𝑒〉 → 𝑎 = 𝑑)) |
12 | 11 | con3d 155 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑐 ∈ 𝑊 ∧ (𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉))) → (¬ 𝑎 = 𝑑 → ¬ 〈𝑎, 𝐵, 𝑐〉 = 〈𝑑, 𝐵, 𝑒〉)) |
13 | 12 | ex 416 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑐 ∈ 𝑊 → ((𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉)) → (¬ 𝑎 = 𝑑 → ¬ 〈𝑎, 𝐵, 𝑐〉 = 〈𝑑, 𝐵, 𝑒〉))) |
14 | 13 | com13 88 |
. . . . . . . . . . . . . . . . . 18
⊢ (¬
𝑎 = 𝑑 → ((𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉)) → (𝑐 ∈ 𝑊 → ¬ 〈𝑎, 𝐵, 𝑐〉 = 〈𝑑, 𝐵, 𝑒〉))) |
15 | 14 | imp31 421 |
. . . . . . . . . . . . . . . . 17
⊢ (((¬
𝑎 = 𝑑 ∧ (𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉))) ∧ 𝑐 ∈ 𝑊) → ¬ 〈𝑎, 𝐵, 𝑐〉 = 〈𝑑, 𝐵, 𝑒〉) |
16 | 15 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢ ((((¬
𝑎 = 𝑑 ∧ (𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉))) ∧ 𝑐 ∈ 𝑊) ∧ 𝑠 ∈ {〈𝑎, 𝐵, 𝑐〉}) → ¬ 〈𝑎, 𝐵, 𝑐〉 = 〈𝑑, 𝐵, 𝑒〉) |
17 | 16 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢
(((((¬ 𝑎 = 𝑑 ∧ (𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉))) ∧ 𝑐 ∈ 𝑊) ∧ 𝑠 ∈ {〈𝑎, 𝐵, 𝑐〉}) ∧ 𝑒 ∈ 𝑊) → ¬ 〈𝑎, 𝐵, 𝑐〉 = 〈𝑑, 𝐵, 𝑒〉) |
18 | | velsn 4532 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑠 ∈ {〈𝑎, 𝐵, 𝑐〉} ↔ 𝑠 = 〈𝑎, 𝐵, 𝑐〉) |
19 | | eqeq1 2742 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑠 = 〈𝑎, 𝐵, 𝑐〉 → (𝑠 = 〈𝑑, 𝐵, 𝑒〉 ↔ 〈𝑎, 𝐵, 𝑐〉 = 〈𝑑, 𝐵, 𝑒〉)) |
20 | 19 | notbid 321 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑠 = 〈𝑎, 𝐵, 𝑐〉 → (¬ 𝑠 = 〈𝑑, 𝐵, 𝑒〉 ↔ ¬ 〈𝑎, 𝐵, 𝑐〉 = 〈𝑑, 𝐵, 𝑒〉)) |
21 | 18, 20 | sylbi 220 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑠 ∈ {〈𝑎, 𝐵, 𝑐〉} → (¬ 𝑠 = 〈𝑑, 𝐵, 𝑒〉 ↔ ¬ 〈𝑎, 𝐵, 𝑐〉 = 〈𝑑, 𝐵, 𝑒〉)) |
22 | 21 | adantl 485 |
. . . . . . . . . . . . . . . 16
⊢ ((((¬
𝑎 = 𝑑 ∧ (𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉))) ∧ 𝑐 ∈ 𝑊) ∧ 𝑠 ∈ {〈𝑎, 𝐵, 𝑐〉}) → (¬ 𝑠 = 〈𝑑, 𝐵, 𝑒〉 ↔ ¬ 〈𝑎, 𝐵, 𝑐〉 = 〈𝑑, 𝐵, 𝑒〉)) |
23 | 22 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢
(((((¬ 𝑎 = 𝑑 ∧ (𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉))) ∧ 𝑐 ∈ 𝑊) ∧ 𝑠 ∈ {〈𝑎, 𝐵, 𝑐〉}) ∧ 𝑒 ∈ 𝑊) → (¬ 𝑠 = 〈𝑑, 𝐵, 𝑒〉 ↔ ¬ 〈𝑎, 𝐵, 𝑐〉 = 〈𝑑, 𝐵, 𝑒〉)) |
24 | 17, 23 | mpbird 260 |
. . . . . . . . . . . . . 14
⊢
(((((¬ 𝑎 = 𝑑 ∧ (𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉))) ∧ 𝑐 ∈ 𝑊) ∧ 𝑠 ∈ {〈𝑎, 𝐵, 𝑐〉}) ∧ 𝑒 ∈ 𝑊) → ¬ 𝑠 = 〈𝑑, 𝐵, 𝑒〉) |
25 | | velsn 4532 |
. . . . . . . . . . . . . 14
⊢ (𝑠 ∈ {〈𝑑, 𝐵, 𝑒〉} ↔ 𝑠 = 〈𝑑, 𝐵, 𝑒〉) |
26 | 24, 25 | sylnibr 332 |
. . . . . . . . . . . . 13
⊢
(((((¬ 𝑎 = 𝑑 ∧ (𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉))) ∧ 𝑐 ∈ 𝑊) ∧ 𝑠 ∈ {〈𝑎, 𝐵, 𝑐〉}) ∧ 𝑒 ∈ 𝑊) → ¬ 𝑠 ∈ {〈𝑑, 𝐵, 𝑒〉}) |
27 | 26 | nrexdv 3180 |
. . . . . . . . . . . 12
⊢ ((((¬
𝑎 = 𝑑 ∧ (𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉))) ∧ 𝑐 ∈ 𝑊) ∧ 𝑠 ∈ {〈𝑎, 𝐵, 𝑐〉}) → ¬ ∃𝑒 ∈ 𝑊 𝑠 ∈ {〈𝑑, 𝐵, 𝑒〉}) |
28 | | eliun 4885 |
. . . . . . . . . . . 12
⊢ (𝑠 ∈ ∪ 𝑒 ∈ 𝑊 {〈𝑑, 𝐵, 𝑒〉} ↔ ∃𝑒 ∈ 𝑊 𝑠 ∈ {〈𝑑, 𝐵, 𝑒〉}) |
29 | 27, 28 | sylnibr 332 |
. . . . . . . . . . 11
⊢ ((((¬
𝑎 = 𝑑 ∧ (𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉))) ∧ 𝑐 ∈ 𝑊) ∧ 𝑠 ∈ {〈𝑎, 𝐵, 𝑐〉}) → ¬ 𝑠 ∈ ∪
𝑒 ∈ 𝑊 {〈𝑑, 𝐵, 𝑒〉}) |
30 | 29 | rexlimdva2 3197 |
. . . . . . . . . 10
⊢ ((¬
𝑎 = 𝑑 ∧ (𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉))) → (∃𝑐 ∈ 𝑊 𝑠 ∈ {〈𝑎, 𝐵, 𝑐〉} → ¬ 𝑠 ∈ ∪
𝑒 ∈ 𝑊 {〈𝑑, 𝐵, 𝑒〉})) |
31 | 3, 30 | syl5bi 245 |
. . . . . . . . 9
⊢ ((¬
𝑎 = 𝑑 ∧ (𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉))) → (𝑠 ∈ ∪
𝑐 ∈ 𝑊 {〈𝑎, 𝐵, 𝑐〉} → ¬ 𝑠 ∈ ∪
𝑒 ∈ 𝑊 {〈𝑑, 𝐵, 𝑒〉})) |
32 | 31 | ralrimiv 3095 |
. . . . . . . 8
⊢ ((¬
𝑎 = 𝑑 ∧ (𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉))) → ∀𝑠 ∈ ∪
𝑐 ∈ 𝑊 {〈𝑎, 𝐵, 𝑐〉} ¬ 𝑠 ∈ ∪
𝑒 ∈ 𝑊 {〈𝑑, 𝐵, 𝑒〉}) |
33 | | oteq3 4772 |
. . . . . . . . . . . . 13
⊢ (𝑐 = 𝑒 → 〈𝑑, 𝐵, 𝑐〉 = 〈𝑑, 𝐵, 𝑒〉) |
34 | 33 | sneqd 4528 |
. . . . . . . . . . . 12
⊢ (𝑐 = 𝑒 → {〈𝑑, 𝐵, 𝑐〉} = {〈𝑑, 𝐵, 𝑒〉}) |
35 | 34 | cbviunv 4926 |
. . . . . . . . . . 11
⊢ ∪ 𝑐 ∈ 𝑊 {〈𝑑, 𝐵, 𝑐〉} = ∪
𝑒 ∈ 𝑊 {〈𝑑, 𝐵, 𝑒〉} |
36 | 35 | eleq2i 2824 |
. . . . . . . . . 10
⊢ (𝑠 ∈ ∪ 𝑐 ∈ 𝑊 {〈𝑑, 𝐵, 𝑐〉} ↔ 𝑠 ∈ ∪
𝑒 ∈ 𝑊 {〈𝑑, 𝐵, 𝑒〉}) |
37 | 36 | notbii 323 |
. . . . . . . . 9
⊢ (¬
𝑠 ∈ ∪ 𝑐 ∈ 𝑊 {〈𝑑, 𝐵, 𝑐〉} ↔ ¬ 𝑠 ∈ ∪
𝑒 ∈ 𝑊 {〈𝑑, 𝐵, 𝑒〉}) |
38 | 37 | ralbii 3080 |
. . . . . . . 8
⊢
(∀𝑠 ∈
∪ 𝑐 ∈ 𝑊 {〈𝑎, 𝐵, 𝑐〉} ¬ 𝑠 ∈ ∪
𝑐 ∈ 𝑊 {〈𝑑, 𝐵, 𝑐〉} ↔ ∀𝑠 ∈ ∪
𝑐 ∈ 𝑊 {〈𝑎, 𝐵, 𝑐〉} ¬ 𝑠 ∈ ∪
𝑒 ∈ 𝑊 {〈𝑑, 𝐵, 𝑒〉}) |
39 | 32, 38 | sylibr 237 |
. . . . . . 7
⊢ ((¬
𝑎 = 𝑑 ∧ (𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉))) → ∀𝑠 ∈ ∪
𝑐 ∈ 𝑊 {〈𝑎, 𝐵, 𝑐〉} ¬ 𝑠 ∈ ∪
𝑐 ∈ 𝑊 {〈𝑑, 𝐵, 𝑐〉}) |
40 | | disj 4337 |
. . . . . . 7
⊢
((∪ 𝑐 ∈ 𝑊 {〈𝑎, 𝐵, 𝑐〉} ∩ ∪ 𝑐 ∈ 𝑊 {〈𝑑, 𝐵, 𝑐〉}) = ∅ ↔ ∀𝑠 ∈ ∪ 𝑐 ∈ 𝑊 {〈𝑎, 𝐵, 𝑐〉} ¬ 𝑠 ∈ ∪
𝑐 ∈ 𝑊 {〈𝑑, 𝐵, 𝑐〉}) |
41 | 39, 40 | sylibr 237 |
. . . . . 6
⊢ ((¬
𝑎 = 𝑑 ∧ (𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉))) → (∪ 𝑐 ∈ 𝑊 {〈𝑎, 𝐵, 𝑐〉} ∩ ∪ 𝑐 ∈ 𝑊 {〈𝑑, 𝐵, 𝑐〉}) = ∅) |
42 | 41 | olcd 873 |
. . . . 5
⊢ ((¬
𝑎 = 𝑑 ∧ (𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉))) → (𝑎 = 𝑑 ∨ (∪
𝑐 ∈ 𝑊 {〈𝑎, 𝐵, 𝑐〉} ∩ ∪ 𝑐 ∈ 𝑊 {〈𝑑, 𝐵, 𝑐〉}) = ∅)) |
43 | 42 | ex 416 |
. . . 4
⊢ (¬
𝑎 = 𝑑 → ((𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉)) → (𝑎 = 𝑑 ∨ (∪
𝑐 ∈ 𝑊 {〈𝑎, 𝐵, 𝑐〉} ∩ ∪ 𝑐 ∈ 𝑊 {〈𝑑, 𝐵, 𝑐〉}) = ∅))) |
44 | 2, 43 | pm2.61i 185 |
. . 3
⊢ ((𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉)) → (𝑎 = 𝑑 ∨ (∪
𝑐 ∈ 𝑊 {〈𝑎, 𝐵, 𝑐〉} ∩ ∪ 𝑐 ∈ 𝑊 {〈𝑑, 𝐵, 𝑐〉}) = ∅)) |
45 | 44 | ralrimivva 3103 |
. 2
⊢ (𝐵 ∈ 𝑋 → ∀𝑎 ∈ 𝑉 ∀𝑑 ∈ 𝑉 (𝑎 = 𝑑 ∨ (∪
𝑐 ∈ 𝑊 {〈𝑎, 𝐵, 𝑐〉} ∩ ∪ 𝑐 ∈ 𝑊 {〈𝑑, 𝐵, 𝑐〉}) = ∅)) |
46 | | oteq1 4770 |
. . . . 5
⊢ (𝑎 = 𝑑 → 〈𝑎, 𝐵, 𝑐〉 = 〈𝑑, 𝐵, 𝑐〉) |
47 | 46 | sneqd 4528 |
. . . 4
⊢ (𝑎 = 𝑑 → {〈𝑎, 𝐵, 𝑐〉} = {〈𝑑, 𝐵, 𝑐〉}) |
48 | 47 | iuneq2d 4910 |
. . 3
⊢ (𝑎 = 𝑑 → ∪
𝑐 ∈ 𝑊 {〈𝑎, 𝐵, 𝑐〉} = ∪
𝑐 ∈ 𝑊 {〈𝑑, 𝐵, 𝑐〉}) |
49 | 48 | disjor 5010 |
. 2
⊢
(Disj 𝑎
∈ 𝑉 ∪ 𝑐 ∈ 𝑊 {〈𝑎, 𝐵, 𝑐〉} ↔ ∀𝑎 ∈ 𝑉 ∀𝑑 ∈ 𝑉 (𝑎 = 𝑑 ∨ (∪
𝑐 ∈ 𝑊 {〈𝑎, 𝐵, 𝑐〉} ∩ ∪ 𝑐 ∈ 𝑊 {〈𝑑, 𝐵, 𝑐〉}) = ∅)) |
50 | 45, 49 | sylibr 237 |
1
⊢ (𝐵 ∈ 𝑋 → Disj 𝑎 ∈ 𝑉 ∪ 𝑐 ∈ 𝑊 {〈𝑎, 𝐵, 𝑐〉}) |