Step | Hyp | Ref
| Expression |
1 | | orc 400 |
. . . . 5
⊢ (𝑎 = 𝑑 → (𝑎 = 𝑑 ∨ (∪
𝑐 ∈ (𝑍 ∖ {𝑎}){〈“𝑎𝐵𝑐”〉} ∩ ∪ 𝑐 ∈ (𝑍 ∖ {𝑑}){〈“𝑑𝐵𝑐”〉}) = ∅)) |
2 | 1 | a1d 25 |
. . . 4
⊢ (𝑎 = 𝑑 → ((𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑌 ∧ 𝑑 ∈ 𝑌)) → (𝑎 = 𝑑 ∨ (∪
𝑐 ∈ (𝑍 ∖ {𝑎}){〈“𝑎𝐵𝑐”〉} ∩ ∪ 𝑐 ∈ (𝑍 ∖ {𝑑}){〈“𝑑𝐵𝑐”〉}) = ∅))) |
3 | | eliun 4524 |
. . . . . . . . . 10
⊢ (𝑠 ∈ ∪ 𝑐 ∈ (𝑍 ∖ {𝑎}){〈“𝑎𝐵𝑐”〉} ↔ ∃𝑐 ∈ (𝑍 ∖ {𝑎})𝑠 ∈ {〈“𝑎𝐵𝑐”〉}) |
4 | | velsn 4193 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑠 ∈ {〈“𝑎𝐵𝑐”〉} ↔ 𝑠 = 〈“𝑎𝐵𝑐”〉) |
5 | | eqeq1 2626 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑠 = 〈“𝑎𝐵𝑐”〉 → (𝑠 = 〈“𝑑𝐵𝑒”〉 ↔ 〈“𝑎𝐵𝑐”〉 = 〈“𝑑𝐵𝑒”〉)) |
6 | 5 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑌 ∧ 𝑑 ∈ 𝑌)) ∧ (𝑐 ∈ (𝑍 ∖ {𝑎}) ∧ 𝑒 ∈ (𝑍 ∖ {𝑑}))) ∧ 𝑠 = 〈“𝑎𝐵𝑐”〉) → (𝑠 = 〈“𝑑𝐵𝑒”〉 ↔ 〈“𝑎𝐵𝑐”〉 = 〈“𝑑𝐵𝑒”〉)) |
7 | | s3cli 13626 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
〈“𝑎𝐵𝑐”〉 ∈ Word V |
8 | | elex 3212 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝐵 ∈ 𝑋 → 𝐵 ∈ V) |
9 | | elex 3212 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑑 ∈ 𝑌 → 𝑑 ∈ V) |
10 | 9 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑎 ∈ 𝑌 ∧ 𝑑 ∈ 𝑌) → 𝑑 ∈ V) |
11 | 8, 10 | anim12ci 591 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑌 ∧ 𝑑 ∈ 𝑌)) → (𝑑 ∈ V ∧ 𝐵 ∈ V)) |
12 | | elex 3212 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑒 ∈ (𝑍 ∖ {𝑑}) → 𝑒 ∈ V) |
13 | 12 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑐 ∈ (𝑍 ∖ {𝑎}) ∧ 𝑒 ∈ (𝑍 ∖ {𝑑})) → 𝑒 ∈ V) |
14 | 11, 13 | anim12i 590 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑌 ∧ 𝑑 ∈ 𝑌)) ∧ (𝑐 ∈ (𝑍 ∖ {𝑎}) ∧ 𝑒 ∈ (𝑍 ∖ {𝑑}))) → ((𝑑 ∈ V ∧ 𝐵 ∈ V) ∧ 𝑒 ∈ V)) |
15 | | df-3an 1039 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑑 ∈ V ∧ 𝐵 ∈ V ∧ 𝑒 ∈ V) ↔ ((𝑑 ∈ V ∧ 𝐵 ∈ V) ∧ 𝑒 ∈ V)) |
16 | 14, 15 | sylibr 224 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑌 ∧ 𝑑 ∈ 𝑌)) ∧ (𝑐 ∈ (𝑍 ∖ {𝑎}) ∧ 𝑒 ∈ (𝑍 ∖ {𝑑}))) → (𝑑 ∈ V ∧ 𝐵 ∈ V ∧ 𝑒 ∈ V)) |
17 | | eqwrds3 13704 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
((〈“𝑎𝐵𝑐”〉 ∈ Word V ∧ (𝑑 ∈ V ∧ 𝐵 ∈ V ∧ 𝑒 ∈ V)) →
(〈“𝑎𝐵𝑐”〉 = 〈“𝑑𝐵𝑒”〉 ↔
((#‘〈“𝑎𝐵𝑐”〉) = 3 ∧ ((〈“𝑎𝐵𝑐”〉‘0) = 𝑑 ∧ (〈“𝑎𝐵𝑐”〉‘1) = 𝐵 ∧ (〈“𝑎𝐵𝑐”〉‘2) = 𝑒)))) |
18 | 7, 16, 17 | sylancr 695 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑌 ∧ 𝑑 ∈ 𝑌)) ∧ (𝑐 ∈ (𝑍 ∖ {𝑎}) ∧ 𝑒 ∈ (𝑍 ∖ {𝑑}))) → (〈“𝑎𝐵𝑐”〉 = 〈“𝑑𝐵𝑒”〉 ↔
((#‘〈“𝑎𝐵𝑐”〉) = 3 ∧ ((〈“𝑎𝐵𝑐”〉‘0) = 𝑑 ∧ (〈“𝑎𝐵𝑐”〉‘1) = 𝐵 ∧ (〈“𝑎𝐵𝑐”〉‘2) = 𝑒)))) |
19 | | vex 3203 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ 𝑎 ∈ V |
20 | | s3fv0 13636 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑎 ∈ V →
(〈“𝑎𝐵𝑐”〉‘0) = 𝑎) |
21 | 19, 20 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(〈“𝑎𝐵𝑐”〉‘0) = 𝑎 |
22 | | simp1 1061 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢
(((〈“𝑎𝐵𝑐”〉‘0) = 𝑑 ∧ (〈“𝑎𝐵𝑐”〉‘1) = 𝐵 ∧ (〈“𝑎𝐵𝑐”〉‘2) = 𝑒) → (〈“𝑎𝐵𝑐”〉‘0) = 𝑑) |
23 | 21, 22 | syl5eqr 2670 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(((〈“𝑎𝐵𝑐”〉‘0) = 𝑑 ∧ (〈“𝑎𝐵𝑐”〉‘1) = 𝐵 ∧ (〈“𝑎𝐵𝑐”〉‘2) = 𝑒) → 𝑎 = 𝑑) |
24 | 23 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(((#‘〈“𝑎𝐵𝑐”〉) = 3 ∧ ((〈“𝑎𝐵𝑐”〉‘0) = 𝑑 ∧ (〈“𝑎𝐵𝑐”〉‘1) = 𝐵 ∧ (〈“𝑎𝐵𝑐”〉‘2) = 𝑒)) → 𝑎 = 𝑑) |
25 | 18, 24 | syl6bi 243 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑌 ∧ 𝑑 ∈ 𝑌)) ∧ (𝑐 ∈ (𝑍 ∖ {𝑎}) ∧ 𝑒 ∈ (𝑍 ∖ {𝑑}))) → (〈“𝑎𝐵𝑐”〉 = 〈“𝑑𝐵𝑒”〉 → 𝑎 = 𝑑)) |
26 | 25 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑌 ∧ 𝑑 ∈ 𝑌)) ∧ (𝑐 ∈ (𝑍 ∖ {𝑎}) ∧ 𝑒 ∈ (𝑍 ∖ {𝑑}))) ∧ 𝑠 = 〈“𝑎𝐵𝑐”〉) → (〈“𝑎𝐵𝑐”〉 = 〈“𝑑𝐵𝑒”〉 → 𝑎 = 𝑑)) |
27 | 6, 26 | sylbid 230 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑌 ∧ 𝑑 ∈ 𝑌)) ∧ (𝑐 ∈ (𝑍 ∖ {𝑎}) ∧ 𝑒 ∈ (𝑍 ∖ {𝑑}))) ∧ 𝑠 = 〈“𝑎𝐵𝑐”〉) → (𝑠 = 〈“𝑑𝐵𝑒”〉 → 𝑎 = 𝑑)) |
28 | 27 | ancoms 469 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑠 = 〈“𝑎𝐵𝑐”〉 ∧ ((𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑌 ∧ 𝑑 ∈ 𝑌)) ∧ (𝑐 ∈ (𝑍 ∖ {𝑎}) ∧ 𝑒 ∈ (𝑍 ∖ {𝑑})))) → (𝑠 = 〈“𝑑𝐵𝑒”〉 → 𝑎 = 𝑑)) |
29 | 28 | con3d 148 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑠 = 〈“𝑎𝐵𝑐”〉 ∧ ((𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑌 ∧ 𝑑 ∈ 𝑌)) ∧ (𝑐 ∈ (𝑍 ∖ {𝑎}) ∧ 𝑒 ∈ (𝑍 ∖ {𝑑})))) → (¬ 𝑎 = 𝑑 → ¬ 𝑠 = 〈“𝑑𝐵𝑒”〉)) |
30 | 29 | exp32 631 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑠 = 〈“𝑎𝐵𝑐”〉 → ((𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑌 ∧ 𝑑 ∈ 𝑌)) → ((𝑐 ∈ (𝑍 ∖ {𝑎}) ∧ 𝑒 ∈ (𝑍 ∖ {𝑑})) → (¬ 𝑎 = 𝑑 → ¬ 𝑠 = 〈“𝑑𝐵𝑒”〉)))) |
31 | 30 | com14 96 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (¬
𝑎 = 𝑑 → ((𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑌 ∧ 𝑑 ∈ 𝑌)) → ((𝑐 ∈ (𝑍 ∖ {𝑎}) ∧ 𝑒 ∈ (𝑍 ∖ {𝑑})) → (𝑠 = 〈“𝑎𝐵𝑐”〉 → ¬ 𝑠 = 〈“𝑑𝐵𝑒”〉)))) |
32 | 31 | imp 445 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((¬
𝑎 = 𝑑 ∧ (𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑌 ∧ 𝑑 ∈ 𝑌))) → ((𝑐 ∈ (𝑍 ∖ {𝑎}) ∧ 𝑒 ∈ (𝑍 ∖ {𝑑})) → (𝑠 = 〈“𝑎𝐵𝑐”〉 → ¬ 𝑠 = 〈“𝑑𝐵𝑒”〉))) |
33 | 32 | expd 452 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((¬
𝑎 = 𝑑 ∧ (𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑌 ∧ 𝑑 ∈ 𝑌))) → (𝑐 ∈ (𝑍 ∖ {𝑎}) → (𝑒 ∈ (𝑍 ∖ {𝑑}) → (𝑠 = 〈“𝑎𝐵𝑐”〉 → ¬ 𝑠 = 〈“𝑑𝐵𝑒”〉)))) |
34 | 33 | com34 91 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((¬
𝑎 = 𝑑 ∧ (𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑌 ∧ 𝑑 ∈ 𝑌))) → (𝑐 ∈ (𝑍 ∖ {𝑎}) → (𝑠 = 〈“𝑎𝐵𝑐”〉 → (𝑒 ∈ (𝑍 ∖ {𝑑}) → ¬ 𝑠 = 〈“𝑑𝐵𝑒”〉)))) |
35 | 34 | imp 445 |
. . . . . . . . . . . . . . . . . 18
⊢ (((¬
𝑎 = 𝑑 ∧ (𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑌 ∧ 𝑑 ∈ 𝑌))) ∧ 𝑐 ∈ (𝑍 ∖ {𝑎})) → (𝑠 = 〈“𝑎𝐵𝑐”〉 → (𝑒 ∈ (𝑍 ∖ {𝑑}) → ¬ 𝑠 = 〈“𝑑𝐵𝑒”〉))) |
36 | 4, 35 | syl5bi 232 |
. . . . . . . . . . . . . . . . 17
⊢ (((¬
𝑎 = 𝑑 ∧ (𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑌 ∧ 𝑑 ∈ 𝑌))) ∧ 𝑐 ∈ (𝑍 ∖ {𝑎})) → (𝑠 ∈ {〈“𝑎𝐵𝑐”〉} → (𝑒 ∈ (𝑍 ∖ {𝑑}) → ¬ 𝑠 = 〈“𝑑𝐵𝑒”〉))) |
37 | 36 | imp 445 |
. . . . . . . . . . . . . . . 16
⊢ ((((¬
𝑎 = 𝑑 ∧ (𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑌 ∧ 𝑑 ∈ 𝑌))) ∧ 𝑐 ∈ (𝑍 ∖ {𝑎})) ∧ 𝑠 ∈ {〈“𝑎𝐵𝑐”〉}) → (𝑒 ∈ (𝑍 ∖ {𝑑}) → ¬ 𝑠 = 〈“𝑑𝐵𝑒”〉)) |
38 | 37 | imp 445 |
. . . . . . . . . . . . . . 15
⊢
(((((¬ 𝑎 = 𝑑 ∧ (𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑌 ∧ 𝑑 ∈ 𝑌))) ∧ 𝑐 ∈ (𝑍 ∖ {𝑎})) ∧ 𝑠 ∈ {〈“𝑎𝐵𝑐”〉}) ∧ 𝑒 ∈ (𝑍 ∖ {𝑑})) → ¬ 𝑠 = 〈“𝑑𝐵𝑒”〉) |
39 | | velsn 4193 |
. . . . . . . . . . . . . . 15
⊢ (𝑠 ∈ {〈“𝑑𝐵𝑒”〉} ↔ 𝑠 = 〈“𝑑𝐵𝑒”〉) |
40 | 38, 39 | sylnibr 319 |
. . . . . . . . . . . . . 14
⊢
(((((¬ 𝑎 = 𝑑 ∧ (𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑌 ∧ 𝑑 ∈ 𝑌))) ∧ 𝑐 ∈ (𝑍 ∖ {𝑎})) ∧ 𝑠 ∈ {〈“𝑎𝐵𝑐”〉}) ∧ 𝑒 ∈ (𝑍 ∖ {𝑑})) → ¬ 𝑠 ∈ {〈“𝑑𝐵𝑒”〉}) |
41 | 40 | nrexdv 3001 |
. . . . . . . . . . . . 13
⊢ ((((¬
𝑎 = 𝑑 ∧ (𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑌 ∧ 𝑑 ∈ 𝑌))) ∧ 𝑐 ∈ (𝑍 ∖ {𝑎})) ∧ 𝑠 ∈ {〈“𝑎𝐵𝑐”〉}) → ¬ ∃𝑒 ∈ (𝑍 ∖ {𝑑})𝑠 ∈ {〈“𝑑𝐵𝑒”〉}) |
42 | | eliun 4524 |
. . . . . . . . . . . . 13
⊢ (𝑠 ∈ ∪ 𝑒 ∈ (𝑍 ∖ {𝑑}){〈“𝑑𝐵𝑒”〉} ↔ ∃𝑒 ∈ (𝑍 ∖ {𝑑})𝑠 ∈ {〈“𝑑𝐵𝑒”〉}) |
43 | 41, 42 | sylnibr 319 |
. . . . . . . . . . . 12
⊢ ((((¬
𝑎 = 𝑑 ∧ (𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑌 ∧ 𝑑 ∈ 𝑌))) ∧ 𝑐 ∈ (𝑍 ∖ {𝑎})) ∧ 𝑠 ∈ {〈“𝑎𝐵𝑐”〉}) → ¬ 𝑠 ∈ ∪ 𝑒 ∈ (𝑍 ∖ {𝑑}){〈“𝑑𝐵𝑒”〉}) |
44 | 43 | ex 450 |
. . . . . . . . . . 11
⊢ (((¬
𝑎 = 𝑑 ∧ (𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑌 ∧ 𝑑 ∈ 𝑌))) ∧ 𝑐 ∈ (𝑍 ∖ {𝑎})) → (𝑠 ∈ {〈“𝑎𝐵𝑐”〉} → ¬ 𝑠 ∈ ∪ 𝑒 ∈ (𝑍 ∖ {𝑑}){〈“𝑑𝐵𝑒”〉})) |
45 | 44 | rexlimdva 3031 |
. . . . . . . . . 10
⊢ ((¬
𝑎 = 𝑑 ∧ (𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑌 ∧ 𝑑 ∈ 𝑌))) → (∃𝑐 ∈ (𝑍 ∖ {𝑎})𝑠 ∈ {〈“𝑎𝐵𝑐”〉} → ¬ 𝑠 ∈ ∪ 𝑒 ∈ (𝑍 ∖ {𝑑}){〈“𝑑𝐵𝑒”〉})) |
46 | 3, 45 | syl5bi 232 |
. . . . . . . . 9
⊢ ((¬
𝑎 = 𝑑 ∧ (𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑌 ∧ 𝑑 ∈ 𝑌))) → (𝑠 ∈ ∪
𝑐 ∈ (𝑍 ∖ {𝑎}){〈“𝑎𝐵𝑐”〉} → ¬ 𝑠 ∈ ∪ 𝑒 ∈ (𝑍 ∖ {𝑑}){〈“𝑑𝐵𝑒”〉})) |
47 | 46 | ralrimiv 2965 |
. . . . . . . 8
⊢ ((¬
𝑎 = 𝑑 ∧ (𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑌 ∧ 𝑑 ∈ 𝑌))) → ∀𝑠 ∈ ∪
𝑐 ∈ (𝑍 ∖ {𝑎}){〈“𝑎𝐵𝑐”〉} ¬ 𝑠 ∈ ∪
𝑒 ∈ (𝑍 ∖ {𝑑}){〈“𝑑𝐵𝑒”〉}) |
48 | | eqidd 2623 |
. . . . . . . . . . . . . 14
⊢ (𝑐 = 𝑒 → 𝑑 = 𝑑) |
49 | | eqidd 2623 |
. . . . . . . . . . . . . 14
⊢ (𝑐 = 𝑒 → 𝐵 = 𝐵) |
50 | | id 22 |
. . . . . . . . . . . . . 14
⊢ (𝑐 = 𝑒 → 𝑐 = 𝑒) |
51 | 48, 49, 50 | s3eqd 13609 |
. . . . . . . . . . . . 13
⊢ (𝑐 = 𝑒 → 〈“𝑑𝐵𝑐”〉 = 〈“𝑑𝐵𝑒”〉) |
52 | 51 | sneqd 4189 |
. . . . . . . . . . . 12
⊢ (𝑐 = 𝑒 → {〈“𝑑𝐵𝑐”〉} = {〈“𝑑𝐵𝑒”〉}) |
53 | 52 | cbviunv 4559 |
. . . . . . . . . . 11
⊢ ∪ 𝑐 ∈ (𝑍 ∖ {𝑑}){〈“𝑑𝐵𝑐”〉} = ∪ 𝑒 ∈ (𝑍 ∖ {𝑑}){〈“𝑑𝐵𝑒”〉} |
54 | 53 | eleq2i 2693 |
. . . . . . . . . 10
⊢ (𝑠 ∈ ∪ 𝑐 ∈ (𝑍 ∖ {𝑑}){〈“𝑑𝐵𝑐”〉} ↔ 𝑠 ∈ ∪
𝑒 ∈ (𝑍 ∖ {𝑑}){〈“𝑑𝐵𝑒”〉}) |
55 | 54 | notbii 310 |
. . . . . . . . 9
⊢ (¬
𝑠 ∈ ∪ 𝑐 ∈ (𝑍 ∖ {𝑑}){〈“𝑑𝐵𝑐”〉} ↔ ¬ 𝑠 ∈ ∪ 𝑒 ∈ (𝑍 ∖ {𝑑}){〈“𝑑𝐵𝑒”〉}) |
56 | 55 | ralbii 2980 |
. . . . . . . 8
⊢
(∀𝑠 ∈
∪ 𝑐 ∈ (𝑍 ∖ {𝑎}){〈“𝑎𝐵𝑐”〉} ¬ 𝑠 ∈ ∪
𝑐 ∈ (𝑍 ∖ {𝑑}){〈“𝑑𝐵𝑐”〉} ↔ ∀𝑠 ∈ ∪ 𝑐 ∈ (𝑍 ∖ {𝑎}){〈“𝑎𝐵𝑐”〉} ¬ 𝑠 ∈ ∪
𝑒 ∈ (𝑍 ∖ {𝑑}){〈“𝑑𝐵𝑒”〉}) |
57 | 47, 56 | sylibr 224 |
. . . . . . 7
⊢ ((¬
𝑎 = 𝑑 ∧ (𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑌 ∧ 𝑑 ∈ 𝑌))) → ∀𝑠 ∈ ∪
𝑐 ∈ (𝑍 ∖ {𝑎}){〈“𝑎𝐵𝑐”〉} ¬ 𝑠 ∈ ∪
𝑐 ∈ (𝑍 ∖ {𝑑}){〈“𝑑𝐵𝑐”〉}) |
58 | | disj 4017 |
. . . . . . 7
⊢
((∪ 𝑐 ∈ (𝑍 ∖ {𝑎}){〈“𝑎𝐵𝑐”〉} ∩ ∪ 𝑐 ∈ (𝑍 ∖ {𝑑}){〈“𝑑𝐵𝑐”〉}) = ∅ ↔
∀𝑠 ∈ ∪ 𝑐 ∈ (𝑍 ∖ {𝑎}){〈“𝑎𝐵𝑐”〉} ¬ 𝑠 ∈ ∪
𝑐 ∈ (𝑍 ∖ {𝑑}){〈“𝑑𝐵𝑐”〉}) |
59 | 57, 58 | sylibr 224 |
. . . . . 6
⊢ ((¬
𝑎 = 𝑑 ∧ (𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑌 ∧ 𝑑 ∈ 𝑌))) → (∪ 𝑐 ∈ (𝑍 ∖ {𝑎}){〈“𝑎𝐵𝑐”〉} ∩ ∪ 𝑐 ∈ (𝑍 ∖ {𝑑}){〈“𝑑𝐵𝑐”〉}) = ∅) |
60 | 59 | olcd 408 |
. . . . 5
⊢ ((¬
𝑎 = 𝑑 ∧ (𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑌 ∧ 𝑑 ∈ 𝑌))) → (𝑎 = 𝑑 ∨ (∪
𝑐 ∈ (𝑍 ∖ {𝑎}){〈“𝑎𝐵𝑐”〉} ∩ ∪ 𝑐 ∈ (𝑍 ∖ {𝑑}){〈“𝑑𝐵𝑐”〉}) = ∅)) |
61 | 60 | ex 450 |
. . . 4
⊢ (¬
𝑎 = 𝑑 → ((𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑌 ∧ 𝑑 ∈ 𝑌)) → (𝑎 = 𝑑 ∨ (∪
𝑐 ∈ (𝑍 ∖ {𝑎}){〈“𝑎𝐵𝑐”〉} ∩ ∪ 𝑐 ∈ (𝑍 ∖ {𝑑}){〈“𝑑𝐵𝑐”〉}) = ∅))) |
62 | 2, 61 | pm2.61i 176 |
. . 3
⊢ ((𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑌 ∧ 𝑑 ∈ 𝑌)) → (𝑎 = 𝑑 ∨ (∪
𝑐 ∈ (𝑍 ∖ {𝑎}){〈“𝑎𝐵𝑐”〉} ∩ ∪ 𝑐 ∈ (𝑍 ∖ {𝑑}){〈“𝑑𝐵𝑐”〉}) = ∅)) |
63 | 62 | ralrimivva 2971 |
. 2
⊢ (𝐵 ∈ 𝑋 → ∀𝑎 ∈ 𝑌 ∀𝑑 ∈ 𝑌 (𝑎 = 𝑑 ∨ (∪
𝑐 ∈ (𝑍 ∖ {𝑎}){〈“𝑎𝐵𝑐”〉} ∩ ∪ 𝑐 ∈ (𝑍 ∖ {𝑑}){〈“𝑑𝐵𝑐”〉}) = ∅)) |
64 | | sneq 4187 |
. . . . 5
⊢ (𝑎 = 𝑑 → {𝑎} = {𝑑}) |
65 | 64 | difeq2d 3728 |
. . . 4
⊢ (𝑎 = 𝑑 → (𝑍 ∖ {𝑎}) = (𝑍 ∖ {𝑑})) |
66 | | id 22 |
. . . . . 6
⊢ (𝑎 = 𝑑 → 𝑎 = 𝑑) |
67 | | eqidd 2623 |
. . . . . 6
⊢ (𝑎 = 𝑑 → 𝐵 = 𝐵) |
68 | | eqidd 2623 |
. . . . . 6
⊢ (𝑎 = 𝑑 → 𝑐 = 𝑐) |
69 | 66, 67, 68 | s3eqd 13609 |
. . . . 5
⊢ (𝑎 = 𝑑 → 〈“𝑎𝐵𝑐”〉 = 〈“𝑑𝐵𝑐”〉) |
70 | 69 | sneqd 4189 |
. . . 4
⊢ (𝑎 = 𝑑 → {〈“𝑎𝐵𝑐”〉} = {〈“𝑑𝐵𝑐”〉}) |
71 | 65, 70 | iuneq12d 4546 |
. . 3
⊢ (𝑎 = 𝑑 → ∪
𝑐 ∈ (𝑍 ∖ {𝑎}){〈“𝑎𝐵𝑐”〉} = ∪ 𝑐 ∈ (𝑍 ∖ {𝑑}){〈“𝑑𝐵𝑐”〉}) |
72 | 71 | disjor 4634 |
. 2
⊢
(Disj 𝑎
∈ 𝑌 ∪ 𝑐 ∈ (𝑍 ∖ {𝑎}){〈“𝑎𝐵𝑐”〉} ↔ ∀𝑎 ∈ 𝑌 ∀𝑑 ∈ 𝑌 (𝑎 = 𝑑 ∨ (∪
𝑐 ∈ (𝑍 ∖ {𝑎}){〈“𝑎𝐵𝑐”〉} ∩ ∪ 𝑐 ∈ (𝑍 ∖ {𝑑}){〈“𝑑𝐵𝑐”〉}) = ∅)) |
73 | 63, 72 | sylibr 224 |
1
⊢ (𝐵 ∈ 𝑋 → Disj 𝑎 ∈ 𝑌 ∪ 𝑐 ∈ (𝑍 ∖ {𝑎}){〈“𝑎𝐵𝑐”〉}) |