| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | eliun 4995 | . . . . . . . . . 10
⊢ (𝑠 ∈ ∪ 𝑐 ∈ (𝑊 ∖ {𝑎}){〈𝑎, 𝐵, 𝑐〉} ↔ ∃𝑐 ∈ (𝑊 ∖ {𝑎})𝑠 ∈ {〈𝑎, 𝐵, 𝑐〉}) | 
| 2 |  | otthg 5490 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑎 ∈ 𝑉 ∧ 𝐵 ∈ 𝑋 ∧ 𝑐 ∈ (𝑊 ∖ {𝑎})) → (〈𝑎, 𝐵, 𝑐〉 = 〈𝑑, 𝐵, 𝑒〉 ↔ (𝑎 = 𝑑 ∧ 𝐵 = 𝐵 ∧ 𝑐 = 𝑒))) | 
| 3 |  | simp1 1137 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑎 = 𝑑 ∧ 𝐵 = 𝐵 ∧ 𝑐 = 𝑒) → 𝑎 = 𝑑) | 
| 4 | 2, 3 | biimtrdi 253 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑎 ∈ 𝑉 ∧ 𝐵 ∈ 𝑋 ∧ 𝑐 ∈ (𝑊 ∖ {𝑎})) → (〈𝑎, 𝐵, 𝑐〉 = 〈𝑑, 𝐵, 𝑒〉 → 𝑎 = 𝑑)) | 
| 5 | 4 | con3d 152 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑎 ∈ 𝑉 ∧ 𝐵 ∈ 𝑋 ∧ 𝑐 ∈ (𝑊 ∖ {𝑎})) → (¬ 𝑎 = 𝑑 → ¬ 〈𝑎, 𝐵, 𝑐〉 = 〈𝑑, 𝐵, 𝑒〉)) | 
| 6 | 5 | 3exp 1120 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑎 ∈ 𝑉 → (𝐵 ∈ 𝑋 → (𝑐 ∈ (𝑊 ∖ {𝑎}) → (¬ 𝑎 = 𝑑 → ¬ 〈𝑎, 𝐵, 𝑐〉 = 〈𝑑, 𝐵, 𝑒〉)))) | 
| 7 | 6 | impcom 407 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝐵 ∈ 𝑋 ∧ 𝑎 ∈ 𝑉) → (𝑐 ∈ (𝑊 ∖ {𝑎}) → (¬ 𝑎 = 𝑑 → ¬ 〈𝑎, 𝐵, 𝑐〉 = 〈𝑑, 𝐵, 𝑒〉))) | 
| 8 | 7 | com3r 87 | . . . . . . . . . . . . . . . . . 18
⊢ (¬
𝑎 = 𝑑 → ((𝐵 ∈ 𝑋 ∧ 𝑎 ∈ 𝑉) → (𝑐 ∈ (𝑊 ∖ {𝑎}) → ¬ 〈𝑎, 𝐵, 𝑐〉 = 〈𝑑, 𝐵, 𝑒〉))) | 
| 9 | 8 | imp31 417 | . . . . . . . . . . . . . . . . 17
⊢ (((¬
𝑎 = 𝑑 ∧ (𝐵 ∈ 𝑋 ∧ 𝑎 ∈ 𝑉)) ∧ 𝑐 ∈ (𝑊 ∖ {𝑎})) → ¬ 〈𝑎, 𝐵, 𝑐〉 = 〈𝑑, 𝐵, 𝑒〉) | 
| 10 |  | velsn 4642 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑠 ∈ {〈𝑎, 𝐵, 𝑐〉} ↔ 𝑠 = 〈𝑎, 𝐵, 𝑐〉) | 
| 11 |  | eqeq1 2741 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑠 = 〈𝑎, 𝐵, 𝑐〉 → (𝑠 = 〈𝑑, 𝐵, 𝑒〉 ↔ 〈𝑎, 𝐵, 𝑐〉 = 〈𝑑, 𝐵, 𝑒〉)) | 
| 12 | 11 | notbid 318 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑠 = 〈𝑎, 𝐵, 𝑐〉 → (¬ 𝑠 = 〈𝑑, 𝐵, 𝑒〉 ↔ ¬ 〈𝑎, 𝐵, 𝑐〉 = 〈𝑑, 𝐵, 𝑒〉)) | 
| 13 | 10, 12 | sylbi 217 | . . . . . . . . . . . . . . . . 17
⊢ (𝑠 ∈ {〈𝑎, 𝐵, 𝑐〉} → (¬ 𝑠 = 〈𝑑, 𝐵, 𝑒〉 ↔ ¬ 〈𝑎, 𝐵, 𝑐〉 = 〈𝑑, 𝐵, 𝑒〉)) | 
| 14 | 9, 13 | syl5ibrcom 247 | . . . . . . . . . . . . . . . 16
⊢ (((¬
𝑎 = 𝑑 ∧ (𝐵 ∈ 𝑋 ∧ 𝑎 ∈ 𝑉)) ∧ 𝑐 ∈ (𝑊 ∖ {𝑎})) → (𝑠 ∈ {〈𝑎, 𝐵, 𝑐〉} → ¬ 𝑠 = 〈𝑑, 𝐵, 𝑒〉)) | 
| 15 | 14 | imp 406 | . . . . . . . . . . . . . . 15
⊢ ((((¬
𝑎 = 𝑑 ∧ (𝐵 ∈ 𝑋 ∧ 𝑎 ∈ 𝑉)) ∧ 𝑐 ∈ (𝑊 ∖ {𝑎})) ∧ 𝑠 ∈ {〈𝑎, 𝐵, 𝑐〉}) → ¬ 𝑠 = 〈𝑑, 𝐵, 𝑒〉) | 
| 16 |  | velsn 4642 | . . . . . . . . . . . . . . 15
⊢ (𝑠 ∈ {〈𝑑, 𝐵, 𝑒〉} ↔ 𝑠 = 〈𝑑, 𝐵, 𝑒〉) | 
| 17 | 15, 16 | sylnibr 329 | . . . . . . . . . . . . . 14
⊢ ((((¬
𝑎 = 𝑑 ∧ (𝐵 ∈ 𝑋 ∧ 𝑎 ∈ 𝑉)) ∧ 𝑐 ∈ (𝑊 ∖ {𝑎})) ∧ 𝑠 ∈ {〈𝑎, 𝐵, 𝑐〉}) → ¬ 𝑠 ∈ {〈𝑑, 𝐵, 𝑒〉}) | 
| 18 | 17 | adantr 480 | . . . . . . . . . . . . 13
⊢
(((((¬ 𝑎 = 𝑑 ∧ (𝐵 ∈ 𝑋 ∧ 𝑎 ∈ 𝑉)) ∧ 𝑐 ∈ (𝑊 ∖ {𝑎})) ∧ 𝑠 ∈ {〈𝑎, 𝐵, 𝑐〉}) ∧ 𝑒 ∈ (𝑊 ∖ {𝑑})) → ¬ 𝑠 ∈ {〈𝑑, 𝐵, 𝑒〉}) | 
| 19 | 18 | nrexdv 3149 | . . . . . . . . . . . 12
⊢ ((((¬
𝑎 = 𝑑 ∧ (𝐵 ∈ 𝑋 ∧ 𝑎 ∈ 𝑉)) ∧ 𝑐 ∈ (𝑊 ∖ {𝑎})) ∧ 𝑠 ∈ {〈𝑎, 𝐵, 𝑐〉}) → ¬ ∃𝑒 ∈ (𝑊 ∖ {𝑑})𝑠 ∈ {〈𝑑, 𝐵, 𝑒〉}) | 
| 20 |  | eliun 4995 | . . . . . . . . . . . 12
⊢ (𝑠 ∈ ∪ 𝑒 ∈ (𝑊 ∖ {𝑑}){〈𝑑, 𝐵, 𝑒〉} ↔ ∃𝑒 ∈ (𝑊 ∖ {𝑑})𝑠 ∈ {〈𝑑, 𝐵, 𝑒〉}) | 
| 21 | 19, 20 | sylnibr 329 | . . . . . . . . . . 11
⊢ ((((¬
𝑎 = 𝑑 ∧ (𝐵 ∈ 𝑋 ∧ 𝑎 ∈ 𝑉)) ∧ 𝑐 ∈ (𝑊 ∖ {𝑎})) ∧ 𝑠 ∈ {〈𝑎, 𝐵, 𝑐〉}) → ¬ 𝑠 ∈ ∪
𝑒 ∈ (𝑊 ∖ {𝑑}){〈𝑑, 𝐵, 𝑒〉}) | 
| 22 | 21 | rexlimdva2 3157 | . . . . . . . . . 10
⊢ ((¬
𝑎 = 𝑑 ∧ (𝐵 ∈ 𝑋 ∧ 𝑎 ∈ 𝑉)) → (∃𝑐 ∈ (𝑊 ∖ {𝑎})𝑠 ∈ {〈𝑎, 𝐵, 𝑐〉} → ¬ 𝑠 ∈ ∪
𝑒 ∈ (𝑊 ∖ {𝑑}){〈𝑑, 𝐵, 𝑒〉})) | 
| 23 | 1, 22 | biimtrid 242 | . . . . . . . . 9
⊢ ((¬
𝑎 = 𝑑 ∧ (𝐵 ∈ 𝑋 ∧ 𝑎 ∈ 𝑉)) → (𝑠 ∈ ∪
𝑐 ∈ (𝑊 ∖ {𝑎}){〈𝑎, 𝐵, 𝑐〉} → ¬ 𝑠 ∈ ∪
𝑒 ∈ (𝑊 ∖ {𝑑}){〈𝑑, 𝐵, 𝑒〉})) | 
| 24 | 23 | ralrimiv 3145 | . . . . . . . 8
⊢ ((¬
𝑎 = 𝑑 ∧ (𝐵 ∈ 𝑋 ∧ 𝑎 ∈ 𝑉)) → ∀𝑠 ∈ ∪
𝑐 ∈ (𝑊 ∖ {𝑎}){〈𝑎, 𝐵, 𝑐〉} ¬ 𝑠 ∈ ∪
𝑒 ∈ (𝑊 ∖ {𝑑}){〈𝑑, 𝐵, 𝑒〉}) | 
| 25 |  | oteq3 4884 | . . . . . . . . . . . . 13
⊢ (𝑐 = 𝑒 → 〈𝑑, 𝐵, 𝑐〉 = 〈𝑑, 𝐵, 𝑒〉) | 
| 26 | 25 | sneqd 4638 | . . . . . . . . . . . 12
⊢ (𝑐 = 𝑒 → {〈𝑑, 𝐵, 𝑐〉} = {〈𝑑, 𝐵, 𝑒〉}) | 
| 27 | 26 | cbviunv 5040 | . . . . . . . . . . 11
⊢ ∪ 𝑐 ∈ (𝑊 ∖ {𝑑}){〈𝑑, 𝐵, 𝑐〉} = ∪
𝑒 ∈ (𝑊 ∖ {𝑑}){〈𝑑, 𝐵, 𝑒〉} | 
| 28 | 27 | eleq2i 2833 | . . . . . . . . . 10
⊢ (𝑠 ∈ ∪ 𝑐 ∈ (𝑊 ∖ {𝑑}){〈𝑑, 𝐵, 𝑐〉} ↔ 𝑠 ∈ ∪
𝑒 ∈ (𝑊 ∖ {𝑑}){〈𝑑, 𝐵, 𝑒〉}) | 
| 29 | 28 | notbii 320 | . . . . . . . . 9
⊢ (¬
𝑠 ∈ ∪ 𝑐 ∈ (𝑊 ∖ {𝑑}){〈𝑑, 𝐵, 𝑐〉} ↔ ¬ 𝑠 ∈ ∪
𝑒 ∈ (𝑊 ∖ {𝑑}){〈𝑑, 𝐵, 𝑒〉}) | 
| 30 | 29 | ralbii 3093 | . . . . . . . 8
⊢
(∀𝑠 ∈
∪ 𝑐 ∈ (𝑊 ∖ {𝑎}){〈𝑎, 𝐵, 𝑐〉} ¬ 𝑠 ∈ ∪
𝑐 ∈ (𝑊 ∖ {𝑑}){〈𝑑, 𝐵, 𝑐〉} ↔ ∀𝑠 ∈ ∪
𝑐 ∈ (𝑊 ∖ {𝑎}){〈𝑎, 𝐵, 𝑐〉} ¬ 𝑠 ∈ ∪
𝑒 ∈ (𝑊 ∖ {𝑑}){〈𝑑, 𝐵, 𝑒〉}) | 
| 31 | 24, 30 | sylibr 234 | . . . . . . 7
⊢ ((¬
𝑎 = 𝑑 ∧ (𝐵 ∈ 𝑋 ∧ 𝑎 ∈ 𝑉)) → ∀𝑠 ∈ ∪
𝑐 ∈ (𝑊 ∖ {𝑎}){〈𝑎, 𝐵, 𝑐〉} ¬ 𝑠 ∈ ∪
𝑐 ∈ (𝑊 ∖ {𝑑}){〈𝑑, 𝐵, 𝑐〉}) | 
| 32 |  | disj 4450 | . . . . . . 7
⊢
((∪ 𝑐 ∈ (𝑊 ∖ {𝑎}){〈𝑎, 𝐵, 𝑐〉} ∩ ∪ 𝑐 ∈ (𝑊 ∖ {𝑑}){〈𝑑, 𝐵, 𝑐〉}) = ∅ ↔ ∀𝑠 ∈ ∪ 𝑐 ∈ (𝑊 ∖ {𝑎}){〈𝑎, 𝐵, 𝑐〉} ¬ 𝑠 ∈ ∪
𝑐 ∈ (𝑊 ∖ {𝑑}){〈𝑑, 𝐵, 𝑐〉}) | 
| 33 | 31, 32 | sylibr 234 | . . . . . 6
⊢ ((¬
𝑎 = 𝑑 ∧ (𝐵 ∈ 𝑋 ∧ 𝑎 ∈ 𝑉)) → (∪ 𝑐 ∈ (𝑊 ∖ {𝑎}){〈𝑎, 𝐵, 𝑐〉} ∩ ∪ 𝑐 ∈ (𝑊 ∖ {𝑑}){〈𝑑, 𝐵, 𝑐〉}) = ∅) | 
| 34 | 33 | expcom 413 | . . . . 5
⊢ ((𝐵 ∈ 𝑋 ∧ 𝑎 ∈ 𝑉) → (¬ 𝑎 = 𝑑 → (∪
𝑐 ∈ (𝑊 ∖ {𝑎}){〈𝑎, 𝐵, 𝑐〉} ∩ ∪ 𝑐 ∈ (𝑊 ∖ {𝑑}){〈𝑑, 𝐵, 𝑐〉}) = ∅)) | 
| 35 | 34 | orrd 864 | . . . 4
⊢ ((𝐵 ∈ 𝑋 ∧ 𝑎 ∈ 𝑉) → (𝑎 = 𝑑 ∨ (∪
𝑐 ∈ (𝑊 ∖ {𝑎}){〈𝑎, 𝐵, 𝑐〉} ∩ ∪ 𝑐 ∈ (𝑊 ∖ {𝑑}){〈𝑑, 𝐵, 𝑐〉}) = ∅)) | 
| 36 | 35 | adantrr 717 | . . 3
⊢ ((𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑉 ∧ 𝑑 ∈ 𝑉)) → (𝑎 = 𝑑 ∨ (∪
𝑐 ∈ (𝑊 ∖ {𝑎}){〈𝑎, 𝐵, 𝑐〉} ∩ ∪ 𝑐 ∈ (𝑊 ∖ {𝑑}){〈𝑑, 𝐵, 𝑐〉}) = ∅)) | 
| 37 | 36 | ralrimivva 3202 | . 2
⊢ (𝐵 ∈ 𝑋 → ∀𝑎 ∈ 𝑉 ∀𝑑 ∈ 𝑉 (𝑎 = 𝑑 ∨ (∪
𝑐 ∈ (𝑊 ∖ {𝑎}){〈𝑎, 𝐵, 𝑐〉} ∩ ∪ 𝑐 ∈ (𝑊 ∖ {𝑑}){〈𝑑, 𝐵, 𝑐〉}) = ∅)) | 
| 38 |  | sneq 4636 | . . . 4
⊢ (𝑎 = 𝑑 → {𝑎} = {𝑑}) | 
| 39 | 38 | difeq2d 4126 | . . 3
⊢ (𝑎 = 𝑑 → (𝑊 ∖ {𝑎}) = (𝑊 ∖ {𝑑})) | 
| 40 |  | oteq1 4882 | . . . 4
⊢ (𝑎 = 𝑑 → 〈𝑎, 𝐵, 𝑐〉 = 〈𝑑, 𝐵, 𝑐〉) | 
| 41 | 40 | sneqd 4638 | . . 3
⊢ (𝑎 = 𝑑 → {〈𝑎, 𝐵, 𝑐〉} = {〈𝑑, 𝐵, 𝑐〉}) | 
| 42 | 39, 41 | disjiunb 5133 | . 2
⊢
(Disj 𝑎
∈ 𝑉 ∪ 𝑐 ∈ (𝑊 ∖ {𝑎}){〈𝑎, 𝐵, 𝑐〉} ↔ ∀𝑎 ∈ 𝑉 ∀𝑑 ∈ 𝑉 (𝑎 = 𝑑 ∨ (∪
𝑐 ∈ (𝑊 ∖ {𝑎}){〈𝑎, 𝐵, 𝑐〉} ∩ ∪ 𝑐 ∈ (𝑊 ∖ {𝑑}){〈𝑑, 𝐵, 𝑐〉}) = ∅)) | 
| 43 | 37, 42 | sylibr 234 | 1
⊢ (𝐵 ∈ 𝑋 → Disj 𝑎 ∈ 𝑉 ∪ 𝑐 ∈ (𝑊 ∖ {𝑎}){〈𝑎, 𝐵, 𝑐〉}) |