| Step | Hyp | Ref
| Expression |
| 1 | | orc 868 |
. . . . 5
⊢ (𝑎 = 𝑑 → (𝑎 = 𝑑 ∨ (∪
𝑐 ∈ (𝑍 ∖ {𝑎}){〈“𝑎𝐵𝑐”〉} ∩ ∪ 𝑐 ∈ (𝑍 ∖ {𝑑}){〈“𝑑𝐵𝑐”〉}) = ∅)) |
| 2 | 1 | a1d 25 |
. . . 4
⊢ (𝑎 = 𝑑 → ((𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑌 ∧ 𝑑 ∈ 𝑌)) → (𝑎 = 𝑑 ∨ (∪
𝑐 ∈ (𝑍 ∖ {𝑎}){〈“𝑎𝐵𝑐”〉} ∩ ∪ 𝑐 ∈ (𝑍 ∖ {𝑑}){〈“𝑑𝐵𝑐”〉}) = ∅))) |
| 3 | | eliun 4995 |
. . . . . . . . . 10
⊢ (𝑠 ∈ ∪ 𝑐 ∈ (𝑍 ∖ {𝑎}){〈“𝑎𝐵𝑐”〉} ↔ ∃𝑐 ∈ (𝑍 ∖ {𝑎})𝑠 ∈ {〈“𝑎𝐵𝑐”〉}) |
| 4 | | velsn 4642 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑠 ∈ {〈“𝑎𝐵𝑐”〉} ↔ 𝑠 = 〈“𝑎𝐵𝑐”〉) |
| 5 | | eqeq1 2741 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑠 = 〈“𝑎𝐵𝑐”〉 → (𝑠 = 〈“𝑑𝐵𝑒”〉 ↔ 〈“𝑎𝐵𝑐”〉 = 〈“𝑑𝐵𝑒”〉)) |
| 6 | 5 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑌 ∧ 𝑑 ∈ 𝑌)) ∧ (𝑐 ∈ (𝑍 ∖ {𝑎}) ∧ 𝑒 ∈ (𝑍 ∖ {𝑑}))) ∧ 𝑠 = 〈“𝑎𝐵𝑐”〉) → (𝑠 = 〈“𝑑𝐵𝑒”〉 ↔ 〈“𝑎𝐵𝑐”〉 = 〈“𝑑𝐵𝑒”〉)) |
| 7 | | s3cli 14920 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
〈“𝑎𝐵𝑐”〉 ∈ Word V |
| 8 | | elex 3501 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝐵 ∈ 𝑋 → 𝐵 ∈ V) |
| 9 | | elex 3501 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑑 ∈ 𝑌 → 𝑑 ∈ V) |
| 10 | 9 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑎 ∈ 𝑌 ∧ 𝑑 ∈ 𝑌) → 𝑑 ∈ V) |
| 11 | 8, 10 | anim12ci 614 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑌 ∧ 𝑑 ∈ 𝑌)) → (𝑑 ∈ V ∧ 𝐵 ∈ V)) |
| 12 | | elex 3501 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑒 ∈ (𝑍 ∖ {𝑑}) → 𝑒 ∈ V) |
| 13 | 12 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑐 ∈ (𝑍 ∖ {𝑎}) ∧ 𝑒 ∈ (𝑍 ∖ {𝑑})) → 𝑒 ∈ V) |
| 14 | 11, 13 | anim12i 613 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑌 ∧ 𝑑 ∈ 𝑌)) ∧ (𝑐 ∈ (𝑍 ∖ {𝑎}) ∧ 𝑒 ∈ (𝑍 ∖ {𝑑}))) → ((𝑑 ∈ V ∧ 𝐵 ∈ V) ∧ 𝑒 ∈ V)) |
| 15 | | df-3an 1089 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑑 ∈ V ∧ 𝐵 ∈ V ∧ 𝑒 ∈ V) ↔ ((𝑑 ∈ V ∧ 𝐵 ∈ V) ∧ 𝑒 ∈ V)) |
| 16 | 14, 15 | sylibr 234 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑌 ∧ 𝑑 ∈ 𝑌)) ∧ (𝑐 ∈ (𝑍 ∖ {𝑎}) ∧ 𝑒 ∈ (𝑍 ∖ {𝑑}))) → (𝑑 ∈ V ∧ 𝐵 ∈ V ∧ 𝑒 ∈ V)) |
| 17 | | eqwrds3 15000 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
((〈“𝑎𝐵𝑐”〉 ∈ Word V ∧ (𝑑 ∈ V ∧ 𝐵 ∈ V ∧ 𝑒 ∈ V)) →
(〈“𝑎𝐵𝑐”〉 = 〈“𝑑𝐵𝑒”〉 ↔
((♯‘〈“𝑎𝐵𝑐”〉) = 3 ∧ ((〈“𝑎𝐵𝑐”〉‘0) = 𝑑 ∧ (〈“𝑎𝐵𝑐”〉‘1) = 𝐵 ∧ (〈“𝑎𝐵𝑐”〉‘2) = 𝑒)))) |
| 18 | 7, 16, 17 | sylancr 587 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑌 ∧ 𝑑 ∈ 𝑌)) ∧ (𝑐 ∈ (𝑍 ∖ {𝑎}) ∧ 𝑒 ∈ (𝑍 ∖ {𝑑}))) → (〈“𝑎𝐵𝑐”〉 = 〈“𝑑𝐵𝑒”〉 ↔
((♯‘〈“𝑎𝐵𝑐”〉) = 3 ∧ ((〈“𝑎𝐵𝑐”〉‘0) = 𝑑 ∧ (〈“𝑎𝐵𝑐”〉‘1) = 𝐵 ∧ (〈“𝑎𝐵𝑐”〉‘2) = 𝑒)))) |
| 19 | | s3fv0 14930 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑎 ∈ V →
(〈“𝑎𝐵𝑐”〉‘0) = 𝑎) |
| 20 | 19 | elv 3485 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(〈“𝑎𝐵𝑐”〉‘0) = 𝑎 |
| 21 | | simp1 1137 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(((〈“𝑎𝐵𝑐”〉‘0) = 𝑑 ∧ (〈“𝑎𝐵𝑐”〉‘1) = 𝐵 ∧ (〈“𝑎𝐵𝑐”〉‘2) = 𝑒) → (〈“𝑎𝐵𝑐”〉‘0) = 𝑑) |
| 22 | 20, 21 | eqtr3id 2791 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(((〈“𝑎𝐵𝑐”〉‘0) = 𝑑 ∧ (〈“𝑎𝐵𝑐”〉‘1) = 𝐵 ∧ (〈“𝑎𝐵𝑐”〉‘2) = 𝑒) → 𝑎 = 𝑑) |
| 23 | 22 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((♯‘〈“𝑎𝐵𝑐”〉) = 3 ∧ ((〈“𝑎𝐵𝑐”〉‘0) = 𝑑 ∧ (〈“𝑎𝐵𝑐”〉‘1) = 𝐵 ∧ (〈“𝑎𝐵𝑐”〉‘2) = 𝑒)) → 𝑎 = 𝑑) |
| 24 | 18, 23 | biimtrdi 253 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑌 ∧ 𝑑 ∈ 𝑌)) ∧ (𝑐 ∈ (𝑍 ∖ {𝑎}) ∧ 𝑒 ∈ (𝑍 ∖ {𝑑}))) → (〈“𝑎𝐵𝑐”〉 = 〈“𝑑𝐵𝑒”〉 → 𝑎 = 𝑑)) |
| 25 | 24 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑌 ∧ 𝑑 ∈ 𝑌)) ∧ (𝑐 ∈ (𝑍 ∖ {𝑎}) ∧ 𝑒 ∈ (𝑍 ∖ {𝑑}))) ∧ 𝑠 = 〈“𝑎𝐵𝑐”〉) → (〈“𝑎𝐵𝑐”〉 = 〈“𝑑𝐵𝑒”〉 → 𝑎 = 𝑑)) |
| 26 | 6, 25 | sylbid 240 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑌 ∧ 𝑑 ∈ 𝑌)) ∧ (𝑐 ∈ (𝑍 ∖ {𝑎}) ∧ 𝑒 ∈ (𝑍 ∖ {𝑑}))) ∧ 𝑠 = 〈“𝑎𝐵𝑐”〉) → (𝑠 = 〈“𝑑𝐵𝑒”〉 → 𝑎 = 𝑑)) |
| 27 | 26 | ancoms 458 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑠 = 〈“𝑎𝐵𝑐”〉 ∧ ((𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑌 ∧ 𝑑 ∈ 𝑌)) ∧ (𝑐 ∈ (𝑍 ∖ {𝑎}) ∧ 𝑒 ∈ (𝑍 ∖ {𝑑})))) → (𝑠 = 〈“𝑑𝐵𝑒”〉 → 𝑎 = 𝑑)) |
| 28 | 27 | con3d 152 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑠 = 〈“𝑎𝐵𝑐”〉 ∧ ((𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑌 ∧ 𝑑 ∈ 𝑌)) ∧ (𝑐 ∈ (𝑍 ∖ {𝑎}) ∧ 𝑒 ∈ (𝑍 ∖ {𝑑})))) → (¬ 𝑎 = 𝑑 → ¬ 𝑠 = 〈“𝑑𝐵𝑒”〉)) |
| 29 | 28 | exp32 420 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑠 = 〈“𝑎𝐵𝑐”〉 → ((𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑌 ∧ 𝑑 ∈ 𝑌)) → ((𝑐 ∈ (𝑍 ∖ {𝑎}) ∧ 𝑒 ∈ (𝑍 ∖ {𝑑})) → (¬ 𝑎 = 𝑑 → ¬ 𝑠 = 〈“𝑑𝐵𝑒”〉)))) |
| 30 | 29 | com14 96 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (¬
𝑎 = 𝑑 → ((𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑌 ∧ 𝑑 ∈ 𝑌)) → ((𝑐 ∈ (𝑍 ∖ {𝑎}) ∧ 𝑒 ∈ (𝑍 ∖ {𝑑})) → (𝑠 = 〈“𝑎𝐵𝑐”〉 → ¬ 𝑠 = 〈“𝑑𝐵𝑒”〉)))) |
| 31 | 30 | imp 406 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((¬
𝑎 = 𝑑 ∧ (𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑌 ∧ 𝑑 ∈ 𝑌))) → ((𝑐 ∈ (𝑍 ∖ {𝑎}) ∧ 𝑒 ∈ (𝑍 ∖ {𝑑})) → (𝑠 = 〈“𝑎𝐵𝑐”〉 → ¬ 𝑠 = 〈“𝑑𝐵𝑒”〉))) |
| 32 | 31 | expd 415 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((¬
𝑎 = 𝑑 ∧ (𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑌 ∧ 𝑑 ∈ 𝑌))) → (𝑐 ∈ (𝑍 ∖ {𝑎}) → (𝑒 ∈ (𝑍 ∖ {𝑑}) → (𝑠 = 〈“𝑎𝐵𝑐”〉 → ¬ 𝑠 = 〈“𝑑𝐵𝑒”〉)))) |
| 33 | 32 | com34 91 |
. . . . . . . . . . . . . . . . . 18
⊢ ((¬
𝑎 = 𝑑 ∧ (𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑌 ∧ 𝑑 ∈ 𝑌))) → (𝑐 ∈ (𝑍 ∖ {𝑎}) → (𝑠 = 〈“𝑎𝐵𝑐”〉 → (𝑒 ∈ (𝑍 ∖ {𝑑}) → ¬ 𝑠 = 〈“𝑑𝐵𝑒”〉)))) |
| 34 | 33 | imp 406 |
. . . . . . . . . . . . . . . . 17
⊢ (((¬
𝑎 = 𝑑 ∧ (𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑌 ∧ 𝑑 ∈ 𝑌))) ∧ 𝑐 ∈ (𝑍 ∖ {𝑎})) → (𝑠 = 〈“𝑎𝐵𝑐”〉 → (𝑒 ∈ (𝑍 ∖ {𝑑}) → ¬ 𝑠 = 〈“𝑑𝐵𝑒”〉))) |
| 35 | 4, 34 | biimtrid 242 |
. . . . . . . . . . . . . . . 16
⊢ (((¬
𝑎 = 𝑑 ∧ (𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑌 ∧ 𝑑 ∈ 𝑌))) ∧ 𝑐 ∈ (𝑍 ∖ {𝑎})) → (𝑠 ∈ {〈“𝑎𝐵𝑐”〉} → (𝑒 ∈ (𝑍 ∖ {𝑑}) → ¬ 𝑠 = 〈“𝑑𝐵𝑒”〉))) |
| 36 | 35 | imp 406 |
. . . . . . . . . . . . . . 15
⊢ ((((¬
𝑎 = 𝑑 ∧ (𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑌 ∧ 𝑑 ∈ 𝑌))) ∧ 𝑐 ∈ (𝑍 ∖ {𝑎})) ∧ 𝑠 ∈ {〈“𝑎𝐵𝑐”〉}) → (𝑒 ∈ (𝑍 ∖ {𝑑}) → ¬ 𝑠 = 〈“𝑑𝐵𝑒”〉)) |
| 37 | 36 | imp 406 |
. . . . . . . . . . . . . 14
⊢
(((((¬ 𝑎 = 𝑑 ∧ (𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑌 ∧ 𝑑 ∈ 𝑌))) ∧ 𝑐 ∈ (𝑍 ∖ {𝑎})) ∧ 𝑠 ∈ {〈“𝑎𝐵𝑐”〉}) ∧ 𝑒 ∈ (𝑍 ∖ {𝑑})) → ¬ 𝑠 = 〈“𝑑𝐵𝑒”〉) |
| 38 | | velsn 4642 |
. . . . . . . . . . . . . 14
⊢ (𝑠 ∈ {〈“𝑑𝐵𝑒”〉} ↔ 𝑠 = 〈“𝑑𝐵𝑒”〉) |
| 39 | 37, 38 | sylnibr 329 |
. . . . . . . . . . . . 13
⊢
(((((¬ 𝑎 = 𝑑 ∧ (𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑌 ∧ 𝑑 ∈ 𝑌))) ∧ 𝑐 ∈ (𝑍 ∖ {𝑎})) ∧ 𝑠 ∈ {〈“𝑎𝐵𝑐”〉}) ∧ 𝑒 ∈ (𝑍 ∖ {𝑑})) → ¬ 𝑠 ∈ {〈“𝑑𝐵𝑒”〉}) |
| 40 | 39 | nrexdv 3149 |
. . . . . . . . . . . 12
⊢ ((((¬
𝑎 = 𝑑 ∧ (𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑌 ∧ 𝑑 ∈ 𝑌))) ∧ 𝑐 ∈ (𝑍 ∖ {𝑎})) ∧ 𝑠 ∈ {〈“𝑎𝐵𝑐”〉}) → ¬ ∃𝑒 ∈ (𝑍 ∖ {𝑑})𝑠 ∈ {〈“𝑑𝐵𝑒”〉}) |
| 41 | | eliun 4995 |
. . . . . . . . . . . 12
⊢ (𝑠 ∈ ∪ 𝑒 ∈ (𝑍 ∖ {𝑑}){〈“𝑑𝐵𝑒”〉} ↔ ∃𝑒 ∈ (𝑍 ∖ {𝑑})𝑠 ∈ {〈“𝑑𝐵𝑒”〉}) |
| 42 | 40, 41 | sylnibr 329 |
. . . . . . . . . . 11
⊢ ((((¬
𝑎 = 𝑑 ∧ (𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑌 ∧ 𝑑 ∈ 𝑌))) ∧ 𝑐 ∈ (𝑍 ∖ {𝑎})) ∧ 𝑠 ∈ {〈“𝑎𝐵𝑐”〉}) → ¬ 𝑠 ∈ ∪ 𝑒 ∈ (𝑍 ∖ {𝑑}){〈“𝑑𝐵𝑒”〉}) |
| 43 | 42 | rexlimdva2 3157 |
. . . . . . . . . 10
⊢ ((¬
𝑎 = 𝑑 ∧ (𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑌 ∧ 𝑑 ∈ 𝑌))) → (∃𝑐 ∈ (𝑍 ∖ {𝑎})𝑠 ∈ {〈“𝑎𝐵𝑐”〉} → ¬ 𝑠 ∈ ∪ 𝑒 ∈ (𝑍 ∖ {𝑑}){〈“𝑑𝐵𝑒”〉})) |
| 44 | 3, 43 | biimtrid 242 |
. . . . . . . . 9
⊢ ((¬
𝑎 = 𝑑 ∧ (𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑌 ∧ 𝑑 ∈ 𝑌))) → (𝑠 ∈ ∪
𝑐 ∈ (𝑍 ∖ {𝑎}){〈“𝑎𝐵𝑐”〉} → ¬ 𝑠 ∈ ∪ 𝑒 ∈ (𝑍 ∖ {𝑑}){〈“𝑑𝐵𝑒”〉})) |
| 45 | 44 | ralrimiv 3145 |
. . . . . . . 8
⊢ ((¬
𝑎 = 𝑑 ∧ (𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑌 ∧ 𝑑 ∈ 𝑌))) → ∀𝑠 ∈ ∪
𝑐 ∈ (𝑍 ∖ {𝑎}){〈“𝑎𝐵𝑐”〉} ¬ 𝑠 ∈ ∪
𝑒 ∈ (𝑍 ∖ {𝑑}){〈“𝑑𝐵𝑒”〉}) |
| 46 | | eqidd 2738 |
. . . . . . . . . . . . . 14
⊢ (𝑐 = 𝑒 → 𝑑 = 𝑑) |
| 47 | | eqidd 2738 |
. . . . . . . . . . . . . 14
⊢ (𝑐 = 𝑒 → 𝐵 = 𝐵) |
| 48 | | id 22 |
. . . . . . . . . . . . . 14
⊢ (𝑐 = 𝑒 → 𝑐 = 𝑒) |
| 49 | 46, 47, 48 | s3eqd 14903 |
. . . . . . . . . . . . 13
⊢ (𝑐 = 𝑒 → 〈“𝑑𝐵𝑐”〉 = 〈“𝑑𝐵𝑒”〉) |
| 50 | 49 | sneqd 4638 |
. . . . . . . . . . . 12
⊢ (𝑐 = 𝑒 → {〈“𝑑𝐵𝑐”〉} = {〈“𝑑𝐵𝑒”〉}) |
| 51 | 50 | cbviunv 5040 |
. . . . . . . . . . 11
⊢ ∪ 𝑐 ∈ (𝑍 ∖ {𝑑}){〈“𝑑𝐵𝑐”〉} = ∪ 𝑒 ∈ (𝑍 ∖ {𝑑}){〈“𝑑𝐵𝑒”〉} |
| 52 | 51 | eleq2i 2833 |
. . . . . . . . . 10
⊢ (𝑠 ∈ ∪ 𝑐 ∈ (𝑍 ∖ {𝑑}){〈“𝑑𝐵𝑐”〉} ↔ 𝑠 ∈ ∪
𝑒 ∈ (𝑍 ∖ {𝑑}){〈“𝑑𝐵𝑒”〉}) |
| 53 | 52 | notbii 320 |
. . . . . . . . 9
⊢ (¬
𝑠 ∈ ∪ 𝑐 ∈ (𝑍 ∖ {𝑑}){〈“𝑑𝐵𝑐”〉} ↔ ¬ 𝑠 ∈ ∪ 𝑒 ∈ (𝑍 ∖ {𝑑}){〈“𝑑𝐵𝑒”〉}) |
| 54 | 53 | ralbii 3093 |
. . . . . . . 8
⊢
(∀𝑠 ∈
∪ 𝑐 ∈ (𝑍 ∖ {𝑎}){〈“𝑎𝐵𝑐”〉} ¬ 𝑠 ∈ ∪
𝑐 ∈ (𝑍 ∖ {𝑑}){〈“𝑑𝐵𝑐”〉} ↔ ∀𝑠 ∈ ∪ 𝑐 ∈ (𝑍 ∖ {𝑎}){〈“𝑎𝐵𝑐”〉} ¬ 𝑠 ∈ ∪
𝑒 ∈ (𝑍 ∖ {𝑑}){〈“𝑑𝐵𝑒”〉}) |
| 55 | 45, 54 | sylibr 234 |
. . . . . . 7
⊢ ((¬
𝑎 = 𝑑 ∧ (𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑌 ∧ 𝑑 ∈ 𝑌))) → ∀𝑠 ∈ ∪
𝑐 ∈ (𝑍 ∖ {𝑎}){〈“𝑎𝐵𝑐”〉} ¬ 𝑠 ∈ ∪
𝑐 ∈ (𝑍 ∖ {𝑑}){〈“𝑑𝐵𝑐”〉}) |
| 56 | | disj 4450 |
. . . . . . 7
⊢
((∪ 𝑐 ∈ (𝑍 ∖ {𝑎}){〈“𝑎𝐵𝑐”〉} ∩ ∪ 𝑐 ∈ (𝑍 ∖ {𝑑}){〈“𝑑𝐵𝑐”〉}) = ∅ ↔
∀𝑠 ∈ ∪ 𝑐 ∈ (𝑍 ∖ {𝑎}){〈“𝑎𝐵𝑐”〉} ¬ 𝑠 ∈ ∪
𝑐 ∈ (𝑍 ∖ {𝑑}){〈“𝑑𝐵𝑐”〉}) |
| 57 | 55, 56 | sylibr 234 |
. . . . . 6
⊢ ((¬
𝑎 = 𝑑 ∧ (𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑌 ∧ 𝑑 ∈ 𝑌))) → (∪ 𝑐 ∈ (𝑍 ∖ {𝑎}){〈“𝑎𝐵𝑐”〉} ∩ ∪ 𝑐 ∈ (𝑍 ∖ {𝑑}){〈“𝑑𝐵𝑐”〉}) = ∅) |
| 58 | 57 | olcd 875 |
. . . . 5
⊢ ((¬
𝑎 = 𝑑 ∧ (𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑌 ∧ 𝑑 ∈ 𝑌))) → (𝑎 = 𝑑 ∨ (∪
𝑐 ∈ (𝑍 ∖ {𝑎}){〈“𝑎𝐵𝑐”〉} ∩ ∪ 𝑐 ∈ (𝑍 ∖ {𝑑}){〈“𝑑𝐵𝑐”〉}) = ∅)) |
| 59 | 58 | ex 412 |
. . . 4
⊢ (¬
𝑎 = 𝑑 → ((𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑌 ∧ 𝑑 ∈ 𝑌)) → (𝑎 = 𝑑 ∨ (∪
𝑐 ∈ (𝑍 ∖ {𝑎}){〈“𝑎𝐵𝑐”〉} ∩ ∪ 𝑐 ∈ (𝑍 ∖ {𝑑}){〈“𝑑𝐵𝑐”〉}) = ∅))) |
| 60 | 2, 59 | pm2.61i 182 |
. . 3
⊢ ((𝐵 ∈ 𝑋 ∧ (𝑎 ∈ 𝑌 ∧ 𝑑 ∈ 𝑌)) → (𝑎 = 𝑑 ∨ (∪
𝑐 ∈ (𝑍 ∖ {𝑎}){〈“𝑎𝐵𝑐”〉} ∩ ∪ 𝑐 ∈ (𝑍 ∖ {𝑑}){〈“𝑑𝐵𝑐”〉}) = ∅)) |
| 61 | 60 | ralrimivva 3202 |
. 2
⊢ (𝐵 ∈ 𝑋 → ∀𝑎 ∈ 𝑌 ∀𝑑 ∈ 𝑌 (𝑎 = 𝑑 ∨ (∪
𝑐 ∈ (𝑍 ∖ {𝑎}){〈“𝑎𝐵𝑐”〉} ∩ ∪ 𝑐 ∈ (𝑍 ∖ {𝑑}){〈“𝑑𝐵𝑐”〉}) = ∅)) |
| 62 | | sneq 4636 |
. . . 4
⊢ (𝑎 = 𝑑 → {𝑎} = {𝑑}) |
| 63 | 62 | difeq2d 4126 |
. . 3
⊢ (𝑎 = 𝑑 → (𝑍 ∖ {𝑎}) = (𝑍 ∖ {𝑑})) |
| 64 | | id 22 |
. . . . 5
⊢ (𝑎 = 𝑑 → 𝑎 = 𝑑) |
| 65 | | eqidd 2738 |
. . . . 5
⊢ (𝑎 = 𝑑 → 𝐵 = 𝐵) |
| 66 | | eqidd 2738 |
. . . . 5
⊢ (𝑎 = 𝑑 → 𝑐 = 𝑐) |
| 67 | 64, 65, 66 | s3eqd 14903 |
. . . 4
⊢ (𝑎 = 𝑑 → 〈“𝑎𝐵𝑐”〉 = 〈“𝑑𝐵𝑐”〉) |
| 68 | 67 | sneqd 4638 |
. . 3
⊢ (𝑎 = 𝑑 → {〈“𝑎𝐵𝑐”〉} = {〈“𝑑𝐵𝑐”〉}) |
| 69 | 63, 68 | disjiunb 5133 |
. 2
⊢
(Disj 𝑎
∈ 𝑌 ∪ 𝑐 ∈ (𝑍 ∖ {𝑎}){〈“𝑎𝐵𝑐”〉} ↔ ∀𝑎 ∈ 𝑌 ∀𝑑 ∈ 𝑌 (𝑎 = 𝑑 ∨ (∪
𝑐 ∈ (𝑍 ∖ {𝑎}){〈“𝑎𝐵𝑐”〉} ∩ ∪ 𝑐 ∈ (𝑍 ∖ {𝑑}){〈“𝑑𝐵𝑐”〉}) = ∅)) |
| 70 | 61, 69 | sylibr 234 |
1
⊢ (𝐵 ∈ 𝑋 → Disj 𝑎 ∈ 𝑌 ∪ 𝑐 ∈ (𝑍 ∖ {𝑎}){〈“𝑎𝐵𝑐”〉}) |