Step | Hyp | Ref
| Expression |
1 | | orc 900 |
. . . . 5
⊢ (𝑐 = 𝑑 → (𝑐 = 𝑑 ∨ ({〈“𝐴𝐵𝑐”〉} ∩ {〈“𝐴𝐵𝑑”〉}) = ∅)) |
2 | 1 | a1d 25 |
. . . 4
⊢ (𝑐 = 𝑑 → (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ (𝑐 ∈ 𝑍 ∧ 𝑑 ∈ 𝑍)) → (𝑐 = 𝑑 ∨ ({〈“𝐴𝐵𝑐”〉} ∩ {〈“𝐴𝐵𝑑”〉}) = ∅))) |
3 | | s3cli 14003 |
. . . . . . . . . . . 12
⊢
〈“𝐴𝐵𝑐”〉 ∈ Word V |
4 | | elex 3430 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ 𝑋 → 𝐴 ∈ V) |
5 | | elex 3430 |
. . . . . . . . . . . . . . 15
⊢ (𝐵 ∈ 𝑌 → 𝐵 ∈ V) |
6 | 4, 5 | anim12i 608 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) → (𝐴 ∈ V ∧ 𝐵 ∈ V)) |
7 | | elex 3430 |
. . . . . . . . . . . . . . 15
⊢ (𝑑 ∈ 𝑍 → 𝑑 ∈ V) |
8 | 7 | adantl 475 |
. . . . . . . . . . . . . 14
⊢ ((𝑐 ∈ 𝑍 ∧ 𝑑 ∈ 𝑍) → 𝑑 ∈ V) |
9 | 6, 8 | anim12i 608 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ (𝑐 ∈ 𝑍 ∧ 𝑑 ∈ 𝑍)) → ((𝐴 ∈ V ∧ 𝐵 ∈ V) ∧ 𝑑 ∈ V)) |
10 | | df-3an 1115 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝑑 ∈ V) ↔ ((𝐴 ∈ V ∧ 𝐵 ∈ V) ∧ 𝑑 ∈ V)) |
11 | 9, 10 | sylibr 226 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ (𝑐 ∈ 𝑍 ∧ 𝑑 ∈ 𝑍)) → (𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝑑 ∈ V)) |
12 | | eqwrds3 14084 |
. . . . . . . . . . . 12
⊢
((〈“𝐴𝐵𝑐”〉 ∈ Word V ∧ (𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝑑 ∈ V)) →
(〈“𝐴𝐵𝑐”〉 = 〈“𝐴𝐵𝑑”〉 ↔
((♯‘〈“𝐴𝐵𝑐”〉) = 3 ∧ ((〈“𝐴𝐵𝑐”〉‘0) = 𝐴 ∧ (〈“𝐴𝐵𝑐”〉‘1) = 𝐵 ∧ (〈“𝐴𝐵𝑐”〉‘2) = 𝑑)))) |
13 | 3, 11, 12 | sylancr 583 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ (𝑐 ∈ 𝑍 ∧ 𝑑 ∈ 𝑍)) → (〈“𝐴𝐵𝑐”〉 = 〈“𝐴𝐵𝑑”〉 ↔
((♯‘〈“𝐴𝐵𝑐”〉) = 3 ∧ ((〈“𝐴𝐵𝑐”〉‘0) = 𝐴 ∧ (〈“𝐴𝐵𝑐”〉‘1) = 𝐵 ∧ (〈“𝐴𝐵𝑐”〉‘2) = 𝑑)))) |
14 | | vex 3418 |
. . . . . . . . . . . . . 14
⊢ 𝑐 ∈ V |
15 | | s3fv2 14015 |
. . . . . . . . . . . . . 14
⊢ (𝑐 ∈ V →
(〈“𝐴𝐵𝑐”〉‘2) = 𝑐) |
16 | 14, 15 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢
(〈“𝐴𝐵𝑐”〉‘2) = 𝑐 |
17 | | simp3 1174 |
. . . . . . . . . . . . 13
⊢
(((〈“𝐴𝐵𝑐”〉‘0) = 𝐴 ∧ (〈“𝐴𝐵𝑐”〉‘1) = 𝐵 ∧ (〈“𝐴𝐵𝑐”〉‘2) = 𝑑) → (〈“𝐴𝐵𝑐”〉‘2) = 𝑑) |
18 | 16, 17 | syl5eqr 2876 |
. . . . . . . . . . . 12
⊢
(((〈“𝐴𝐵𝑐”〉‘0) = 𝐴 ∧ (〈“𝐴𝐵𝑐”〉‘1) = 𝐵 ∧ (〈“𝐴𝐵𝑐”〉‘2) = 𝑑) → 𝑐 = 𝑑) |
19 | 18 | adantl 475 |
. . . . . . . . . . 11
⊢
(((♯‘〈“𝐴𝐵𝑐”〉) = 3 ∧ ((〈“𝐴𝐵𝑐”〉‘0) = 𝐴 ∧ (〈“𝐴𝐵𝑐”〉‘1) = 𝐵 ∧ (〈“𝐴𝐵𝑐”〉‘2) = 𝑑)) → 𝑐 = 𝑑) |
20 | 13, 19 | syl6bi 245 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ (𝑐 ∈ 𝑍 ∧ 𝑑 ∈ 𝑍)) → (〈“𝐴𝐵𝑐”〉 = 〈“𝐴𝐵𝑑”〉 → 𝑐 = 𝑑)) |
21 | 20 | con3rr3 153 |
. . . . . . . . 9
⊢ (¬
𝑐 = 𝑑 → (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ (𝑐 ∈ 𝑍 ∧ 𝑑 ∈ 𝑍)) → ¬ 〈“𝐴𝐵𝑐”〉 = 〈“𝐴𝐵𝑑”〉)) |
22 | 21 | imp 397 |
. . . . . . . 8
⊢ ((¬
𝑐 = 𝑑 ∧ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ (𝑐 ∈ 𝑍 ∧ 𝑑 ∈ 𝑍))) → ¬ 〈“𝐴𝐵𝑐”〉 = 〈“𝐴𝐵𝑑”〉) |
23 | 22 | neqned 3007 |
. . . . . . 7
⊢ ((¬
𝑐 = 𝑑 ∧ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ (𝑐 ∈ 𝑍 ∧ 𝑑 ∈ 𝑍))) → 〈“𝐴𝐵𝑐”〉 ≠ 〈“𝐴𝐵𝑑”〉) |
24 | | disjsn2 4467 |
. . . . . . 7
⊢
(〈“𝐴𝐵𝑐”〉 ≠ 〈“𝐴𝐵𝑑”〉 → ({〈“𝐴𝐵𝑐”〉} ∩ {〈“𝐴𝐵𝑑”〉}) = ∅) |
25 | 23, 24 | syl 17 |
. . . . . 6
⊢ ((¬
𝑐 = 𝑑 ∧ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ (𝑐 ∈ 𝑍 ∧ 𝑑 ∈ 𝑍))) → ({〈“𝐴𝐵𝑐”〉} ∩ {〈“𝐴𝐵𝑑”〉}) = ∅) |
26 | 25 | olcd 907 |
. . . . 5
⊢ ((¬
𝑐 = 𝑑 ∧ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ (𝑐 ∈ 𝑍 ∧ 𝑑 ∈ 𝑍))) → (𝑐 = 𝑑 ∨ ({〈“𝐴𝐵𝑐”〉} ∩ {〈“𝐴𝐵𝑑”〉}) = ∅)) |
27 | 26 | ex 403 |
. . . 4
⊢ (¬
𝑐 = 𝑑 → (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ (𝑐 ∈ 𝑍 ∧ 𝑑 ∈ 𝑍)) → (𝑐 = 𝑑 ∨ ({〈“𝐴𝐵𝑐”〉} ∩ {〈“𝐴𝐵𝑑”〉}) = ∅))) |
28 | 2, 27 | pm2.61i 177 |
. . 3
⊢ (((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) ∧ (𝑐 ∈ 𝑍 ∧ 𝑑 ∈ 𝑍)) → (𝑐 = 𝑑 ∨ ({〈“𝐴𝐵𝑐”〉} ∩ {〈“𝐴𝐵𝑑”〉}) = ∅)) |
29 | 28 | ralrimivva 3181 |
. 2
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) → ∀𝑐 ∈ 𝑍 ∀𝑑 ∈ 𝑍 (𝑐 = 𝑑 ∨ ({〈“𝐴𝐵𝑐”〉} ∩ {〈“𝐴𝐵𝑑”〉}) = ∅)) |
30 | | eqidd 2827 |
. . . . 5
⊢ (𝑐 = 𝑑 → 𝐴 = 𝐴) |
31 | | eqidd 2827 |
. . . . 5
⊢ (𝑐 = 𝑑 → 𝐵 = 𝐵) |
32 | | id 22 |
. . . . 5
⊢ (𝑐 = 𝑑 → 𝑐 = 𝑑) |
33 | 30, 31, 32 | s3eqd 13986 |
. . . 4
⊢ (𝑐 = 𝑑 → 〈“𝐴𝐵𝑐”〉 = 〈“𝐴𝐵𝑑”〉) |
34 | 33 | sneqd 4410 |
. . 3
⊢ (𝑐 = 𝑑 → {〈“𝐴𝐵𝑐”〉} = {〈“𝐴𝐵𝑑”〉}) |
35 | 34 | disjor 4856 |
. 2
⊢
(Disj 𝑐
∈ 𝑍
{〈“𝐴𝐵𝑐”〉} ↔ ∀𝑐 ∈ 𝑍 ∀𝑑 ∈ 𝑍 (𝑐 = 𝑑 ∨ ({〈“𝐴𝐵𝑐”〉} ∩ {〈“𝐴𝐵𝑑”〉}) = ∅)) |
36 | 29, 35 | sylibr 226 |
1
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌) → Disj 𝑐 ∈ 𝑍 {〈“𝐴𝐵𝑐”〉}) |