Step | Hyp | Ref
| Expression |
1 | | orc 399 |
. . . . 5
⊢ (𝑎 = 𝑑 → (𝑎 = 𝑑 ∨ (∪
𝑐 ∈ 𝑊 {〈𝑎, 𝐵, 𝑐〉} ∩ ∪ 𝑐 ∈ 𝑊 {〈𝑑, 𝐵, 𝑐〉}) = ∅)) |
2 | 1 | a1d 25 |
. . . 4
⊢ (𝑎 = 𝑑 → ((𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉)) → (𝑎 = 𝑑 ∨ (∪
𝑐 ∈ 𝑊 {〈𝑎, 𝐵, 𝑐〉} ∩ ∪ 𝑐 ∈ 𝑊 {〈𝑑, 𝐵, 𝑐〉}) = ∅))) |
3 | | eliun 4460 |
. . . . . . . . . 10
⊢ (𝑠 ∈ ∪ 𝑐 ∈ 𝑊 {〈𝑎, 𝐵, 𝑐〉} ↔ ∃𝑐 ∈ 𝑊 𝑠 ∈ {〈𝑎, 𝐵, 𝑐〉}) |
4 | | simprl 790 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉)) → 𝑎 ∈ 𝑉) |
5 | 4 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑐 ∈ 𝑊 ∧ (𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉))) → 𝑎 ∈ 𝑉) |
6 | | simprl 790 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑐 ∈ 𝑊 ∧ (𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉))) → 𝐵 ∈ 𝑋) |
7 | | simpl 472 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑐 ∈ 𝑊 ∧ (𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉))) → 𝑐 ∈ 𝑊) |
8 | | otthg 4880 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑎 ∈ 𝑉 ∧ 𝐵 ∈ 𝑋 ∧ 𝑐 ∈ 𝑊) → (〈𝑎, 𝐵, 𝑐〉 = 〈𝑑, 𝐵, 𝑒〉 ↔ (𝑎 = 𝑑 ∧ 𝐵 = 𝐵 ∧ 𝑐 = 𝑒))) |
9 | 5, 6, 7, 8 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑐 ∈ 𝑊 ∧ (𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉))) → (〈𝑎, 𝐵, 𝑐〉 = 〈𝑑, 𝐵, 𝑒〉 ↔ (𝑎 = 𝑑 ∧ 𝐵 = 𝐵 ∧ 𝑐 = 𝑒))) |
10 | | simp1 1054 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑎 = 𝑑 ∧ 𝐵 = 𝐵 ∧ 𝑐 = 𝑒) → 𝑎 = 𝑑) |
11 | 9, 10 | syl6bi 242 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑐 ∈ 𝑊 ∧ (𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉))) → (〈𝑎, 𝐵, 𝑐〉 = 〈𝑑, 𝐵, 𝑒〉 → 𝑎 = 𝑑)) |
12 | 11 | con3d 147 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑐 ∈ 𝑊 ∧ (𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉))) → (¬ 𝑎 = 𝑑 → ¬ 〈𝑎, 𝐵, 𝑐〉 = 〈𝑑, 𝐵, 𝑒〉)) |
13 | 12 | ex 449 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑐 ∈ 𝑊 → ((𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉)) → (¬ 𝑎 = 𝑑 → ¬ 〈𝑎, 𝐵, 𝑐〉 = 〈𝑑, 𝐵, 𝑒〉))) |
14 | 13 | com13 86 |
. . . . . . . . . . . . . . . . . . 19
⊢ (¬
𝑎 = 𝑑 → ((𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉)) → (𝑐 ∈ 𝑊 → ¬ 〈𝑎, 𝐵, 𝑐〉 = 〈𝑑, 𝐵, 𝑒〉))) |
15 | 14 | imp31 447 |
. . . . . . . . . . . . . . . . . 18
⊢ (((¬
𝑎 = 𝑑 ∧ (𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉))) ∧ 𝑐 ∈ 𝑊) → ¬ 〈𝑎, 𝐵, 𝑐〉 = 〈𝑑, 𝐵, 𝑒〉) |
16 | 15 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((((¬
𝑎 = 𝑑 ∧ (𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉))) ∧ 𝑐 ∈ 𝑊) ∧ 𝑠 ∈ {〈𝑎, 𝐵, 𝑐〉}) → ¬ 〈𝑎, 𝐵, 𝑐〉 = 〈𝑑, 𝐵, 𝑒〉) |
17 | 16 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢
(((((¬ 𝑎 = 𝑑 ∧ (𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉))) ∧ 𝑐 ∈ 𝑊) ∧ 𝑠 ∈ {〈𝑎, 𝐵, 𝑐〉}) ∧ 𝑒 ∈ 𝑊) → ¬ 〈𝑎, 𝐵, 𝑐〉 = 〈𝑑, 𝐵, 𝑒〉) |
18 | | velsn 4141 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑠 ∈ {〈𝑎, 𝐵, 𝑐〉} ↔ 𝑠 = 〈𝑎, 𝐵, 𝑐〉) |
19 | | eqeq1 2614 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑠 = 〈𝑎, 𝐵, 𝑐〉 → (𝑠 = 〈𝑑, 𝐵, 𝑒〉 ↔ 〈𝑎, 𝐵, 𝑐〉 = 〈𝑑, 𝐵, 𝑒〉)) |
20 | 19 | notbid 307 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑠 = 〈𝑎, 𝐵, 𝑐〉 → (¬ 𝑠 = 〈𝑑, 𝐵, 𝑒〉 ↔ ¬ 〈𝑎, 𝐵, 𝑐〉 = 〈𝑑, 𝐵, 𝑒〉)) |
21 | 18, 20 | sylbi 206 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑠 ∈ {〈𝑎, 𝐵, 𝑐〉} → (¬ 𝑠 = 〈𝑑, 𝐵, 𝑒〉 ↔ ¬ 〈𝑎, 𝐵, 𝑐〉 = 〈𝑑, 𝐵, 𝑒〉)) |
22 | 21 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((((¬
𝑎 = 𝑑 ∧ (𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉))) ∧ 𝑐 ∈ 𝑊) ∧ 𝑠 ∈ {〈𝑎, 𝐵, 𝑐〉}) → (¬ 𝑠 = 〈𝑑, 𝐵, 𝑒〉 ↔ ¬ 〈𝑎, 𝐵, 𝑐〉 = 〈𝑑, 𝐵, 𝑒〉)) |
23 | 22 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢
(((((¬ 𝑎 = 𝑑 ∧ (𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉))) ∧ 𝑐 ∈ 𝑊) ∧ 𝑠 ∈ {〈𝑎, 𝐵, 𝑐〉}) ∧ 𝑒 ∈ 𝑊) → (¬ 𝑠 = 〈𝑑, 𝐵, 𝑒〉 ↔ ¬ 〈𝑎, 𝐵, 𝑐〉 = 〈𝑑, 𝐵, 𝑒〉)) |
24 | 17, 23 | mpbird 246 |
. . . . . . . . . . . . . . 15
⊢
(((((¬ 𝑎 = 𝑑 ∧ (𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉))) ∧ 𝑐 ∈ 𝑊) ∧ 𝑠 ∈ {〈𝑎, 𝐵, 𝑐〉}) ∧ 𝑒 ∈ 𝑊) → ¬ 𝑠 = 〈𝑑, 𝐵, 𝑒〉) |
25 | | velsn 4141 |
. . . . . . . . . . . . . . 15
⊢ (𝑠 ∈ {〈𝑑, 𝐵, 𝑒〉} ↔ 𝑠 = 〈𝑑, 𝐵, 𝑒〉) |
26 | 24, 25 | sylnibr 318 |
. . . . . . . . . . . . . 14
⊢
(((((¬ 𝑎 = 𝑑 ∧ (𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉))) ∧ 𝑐 ∈ 𝑊) ∧ 𝑠 ∈ {〈𝑎, 𝐵, 𝑐〉}) ∧ 𝑒 ∈ 𝑊) → ¬ 𝑠 ∈ {〈𝑑, 𝐵, 𝑒〉}) |
27 | 26 | nrexdv 2984 |
. . . . . . . . . . . . 13
⊢ ((((¬
𝑎 = 𝑑 ∧ (𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉))) ∧ 𝑐 ∈ 𝑊) ∧ 𝑠 ∈ {〈𝑎, 𝐵, 𝑐〉}) → ¬ ∃𝑒 ∈ 𝑊 𝑠 ∈ {〈𝑑, 𝐵, 𝑒〉}) |
28 | | eliun 4460 |
. . . . . . . . . . . . 13
⊢ (𝑠 ∈ ∪ 𝑒 ∈ 𝑊 {〈𝑑, 𝐵, 𝑒〉} ↔ ∃𝑒 ∈ 𝑊 𝑠 ∈ {〈𝑑, 𝐵, 𝑒〉}) |
29 | 27, 28 | sylnibr 318 |
. . . . . . . . . . . 12
⊢ ((((¬
𝑎 = 𝑑 ∧ (𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉))) ∧ 𝑐 ∈ 𝑊) ∧ 𝑠 ∈ {〈𝑎, 𝐵, 𝑐〉}) → ¬ 𝑠 ∈ ∪
𝑒 ∈ 𝑊 {〈𝑑, 𝐵, 𝑒〉}) |
30 | 29 | ex 449 |
. . . . . . . . . . 11
⊢ (((¬
𝑎 = 𝑑 ∧ (𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉))) ∧ 𝑐 ∈ 𝑊) → (𝑠 ∈ {〈𝑎, 𝐵, 𝑐〉} → ¬ 𝑠 ∈ ∪
𝑒 ∈ 𝑊 {〈𝑑, 𝐵, 𝑒〉})) |
31 | 30 | rexlimdva 3013 |
. . . . . . . . . 10
⊢ ((¬
𝑎 = 𝑑 ∧ (𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉))) → (∃𝑐 ∈ 𝑊 𝑠 ∈ {〈𝑎, 𝐵, 𝑐〉} → ¬ 𝑠 ∈ ∪
𝑒 ∈ 𝑊 {〈𝑑, 𝐵, 𝑒〉})) |
32 | 3, 31 | syl5bi 231 |
. . . . . . . . 9
⊢ ((¬
𝑎 = 𝑑 ∧ (𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉))) → (𝑠 ∈ ∪
𝑐 ∈ 𝑊 {〈𝑎, 𝐵, 𝑐〉} → ¬ 𝑠 ∈ ∪
𝑒 ∈ 𝑊 {〈𝑑, 𝐵, 𝑒〉})) |
33 | 32 | ralrimiv 2948 |
. . . . . . . 8
⊢ ((¬
𝑎 = 𝑑 ∧ (𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉))) → ∀𝑠 ∈ ∪
𝑐 ∈ 𝑊 {〈𝑎, 𝐵, 𝑐〉} ¬ 𝑠 ∈ ∪
𝑒 ∈ 𝑊 {〈𝑑, 𝐵, 𝑒〉}) |
34 | | oteq3 4351 |
. . . . . . . . . . . . 13
⊢ (𝑐 = 𝑒 → 〈𝑑, 𝐵, 𝑐〉 = 〈𝑑, 𝐵, 𝑒〉) |
35 | 34 | sneqd 4137 |
. . . . . . . . . . . 12
⊢ (𝑐 = 𝑒 → {〈𝑑, 𝐵, 𝑐〉} = {〈𝑑, 𝐵, 𝑒〉}) |
36 | 35 | cbviunv 4495 |
. . . . . . . . . . 11
⊢ ∪ 𝑐 ∈ 𝑊 {〈𝑑, 𝐵, 𝑐〉} = ∪
𝑒 ∈ 𝑊 {〈𝑑, 𝐵, 𝑒〉} |
37 | 36 | eleq2i 2680 |
. . . . . . . . . 10
⊢ (𝑠 ∈ ∪ 𝑐 ∈ 𝑊 {〈𝑑, 𝐵, 𝑐〉} ↔ 𝑠 ∈ ∪
𝑒 ∈ 𝑊 {〈𝑑, 𝐵, 𝑒〉}) |
38 | 37 | notbii 309 |
. . . . . . . . 9
⊢ (¬
𝑠 ∈ ∪ 𝑐 ∈ 𝑊 {〈𝑑, 𝐵, 𝑐〉} ↔ ¬ 𝑠 ∈ ∪
𝑒 ∈ 𝑊 {〈𝑑, 𝐵, 𝑒〉}) |
39 | 38 | ralbii 2963 |
. . . . . . . 8
⊢
(∀𝑠 ∈
∪ 𝑐 ∈ 𝑊 {〈𝑎, 𝐵, 𝑐〉} ¬ 𝑠 ∈ ∪
𝑐 ∈ 𝑊 {〈𝑑, 𝐵, 𝑐〉} ↔ ∀𝑠 ∈ ∪
𝑐 ∈ 𝑊 {〈𝑎, 𝐵, 𝑐〉} ¬ 𝑠 ∈ ∪
𝑒 ∈ 𝑊 {〈𝑑, 𝐵, 𝑒〉}) |
40 | 33, 39 | sylibr 223 |
. . . . . . 7
⊢ ((¬
𝑎 = 𝑑 ∧ (𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉))) → ∀𝑠 ∈ ∪
𝑐 ∈ 𝑊 {〈𝑎, 𝐵, 𝑐〉} ¬ 𝑠 ∈ ∪
𝑐 ∈ 𝑊 {〈𝑑, 𝐵, 𝑐〉}) |
41 | | disj 3969 |
. . . . . . 7
⊢
((∪ 𝑐 ∈ 𝑊 {〈𝑎, 𝐵, 𝑐〉} ∩ ∪ 𝑐 ∈ 𝑊 {〈𝑑, 𝐵, 𝑐〉}) = ∅ ↔ ∀𝑠 ∈ ∪ 𝑐 ∈ 𝑊 {〈𝑎, 𝐵, 𝑐〉} ¬ 𝑠 ∈ ∪
𝑐 ∈ 𝑊 {〈𝑑, 𝐵, 𝑐〉}) |
42 | 40, 41 | sylibr 223 |
. . . . . 6
⊢ ((¬
𝑎 = 𝑑 ∧ (𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉))) → (∪ 𝑐 ∈ 𝑊 {〈𝑎, 𝐵, 𝑐〉} ∩ ∪ 𝑐 ∈ 𝑊 {〈𝑑, 𝐵, 𝑐〉}) = ∅) |
43 | 42 | olcd 407 |
. . . . 5
⊢ ((¬
𝑎 = 𝑑 ∧ (𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉))) → (𝑎 = 𝑑 ∨ (∪
𝑐 ∈ 𝑊 {〈𝑎, 𝐵, 𝑐〉} ∩ ∪ 𝑐 ∈ 𝑊 {〈𝑑, 𝐵, 𝑐〉}) = ∅)) |
44 | 43 | ex 449 |
. . . 4
⊢ (¬
𝑎 = 𝑑 → ((𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉)) → (𝑎 = 𝑑 ∨ (∪
𝑐 ∈ 𝑊 {〈𝑎, 𝐵, 𝑐〉} ∩ ∪ 𝑐 ∈ 𝑊 {〈𝑑, 𝐵, 𝑐〉}) = ∅))) |
45 | 2, 44 | pm2.61i 175 |
. . 3
⊢ ((𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉)) → (𝑎 = 𝑑 ∨ (∪
𝑐 ∈ 𝑊 {〈𝑎, 𝐵, 𝑐〉} ∩ ∪ 𝑐 ∈ 𝑊 {〈𝑑, 𝐵, 𝑐〉}) = ∅)) |
46 | 45 | ralrimivva 2954 |
. 2
⊢ (𝐵 ∈ 𝑋 → ∀𝑎 ∈ 𝑉 ∀𝑑 ∈ 𝑉 (𝑎 = 𝑑 ∨ (∪
𝑐 ∈ 𝑊 {〈𝑎, 𝐵, 𝑐〉} ∩ ∪ 𝑐 ∈ 𝑊 {〈𝑑, 𝐵, 𝑐〉}) = ∅)) |
47 | | oteq1 4349 |
. . . . 5
⊢ (𝑎 = 𝑑 → 〈𝑎, 𝐵, 𝑐〉 = 〈𝑑, 𝐵, 𝑐〉) |
48 | 47 | sneqd 4137 |
. . . 4
⊢ (𝑎 = 𝑑 → {〈𝑎, 𝐵, 𝑐〉} = {〈𝑑, 𝐵, 𝑐〉}) |
49 | 48 | iuneq2d 4483 |
. . 3
⊢ (𝑎 = 𝑑 → ∪
𝑐 ∈ 𝑊 {〈𝑎, 𝐵, 𝑐〉} = ∪
𝑐 ∈ 𝑊 {〈𝑑, 𝐵, 𝑐〉}) |
50 | 49 | disjor 4567 |
. 2
⊢
(Disj 𝑎
∈ 𝑉 ∪ 𝑐 ∈ 𝑊 {〈𝑎, 𝐵, 𝑐〉} ↔ ∀𝑎 ∈ 𝑉 ∀𝑑 ∈ 𝑉 (𝑎 = 𝑑 ∨ (∪
𝑐 ∈ 𝑊 {〈𝑎, 𝐵, 𝑐〉} ∩ ∪ 𝑐 ∈ 𝑊 {〈𝑑, 𝐵, 𝑐〉}) = ∅)) |
51 | 46, 50 | sylibr 223 |
1
⊢ (𝐵 ∈ 𝑋 → Disj 𝑎 ∈ 𝑉 ∪ 𝑐 ∈ 𝑊 {〈𝑎, 𝐵, 𝑐〉}) |