Step |
Hyp |
Ref |
Expression |
1 |
|
orc |
⊢ ( 𝑐 = 𝑑 → ( 𝑐 = 𝑑 ∨ ( { 〈“ 𝐴 𝐵 𝑐 ”〉 } ∩ { 〈“ 𝐴 𝐵 𝑑 ”〉 } ) = ∅ ) ) |
2 |
1
|
a1d |
⊢ ( 𝑐 = 𝑑 → ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ∧ ( 𝑐 ∈ 𝑍 ∧ 𝑑 ∈ 𝑍 ) ) → ( 𝑐 = 𝑑 ∨ ( { 〈“ 𝐴 𝐵 𝑐 ”〉 } ∩ { 〈“ 𝐴 𝐵 𝑑 ”〉 } ) = ∅ ) ) ) |
3 |
|
s3cli |
⊢ 〈“ 𝐴 𝐵 𝑐 ”〉 ∈ Word V |
4 |
|
elex |
⊢ ( 𝐴 ∈ 𝑋 → 𝐴 ∈ V ) |
5 |
|
elex |
⊢ ( 𝐵 ∈ 𝑌 → 𝐵 ∈ V ) |
6 |
4 5
|
anim12i |
⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ) |
7 |
|
elex |
⊢ ( 𝑑 ∈ 𝑍 → 𝑑 ∈ V ) |
8 |
7
|
adantl |
⊢ ( ( 𝑐 ∈ 𝑍 ∧ 𝑑 ∈ 𝑍 ) → 𝑑 ∈ V ) |
9 |
6 8
|
anim12i |
⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ∧ ( 𝑐 ∈ 𝑍 ∧ 𝑑 ∈ 𝑍 ) ) → ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ 𝑑 ∈ V ) ) |
10 |
|
df-3an |
⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝑑 ∈ V ) ↔ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ∧ 𝑑 ∈ V ) ) |
11 |
9 10
|
sylibr |
⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ∧ ( 𝑐 ∈ 𝑍 ∧ 𝑑 ∈ 𝑍 ) ) → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝑑 ∈ V ) ) |
12 |
|
eqwrds3 |
⊢ ( ( 〈“ 𝐴 𝐵 𝑐 ”〉 ∈ Word V ∧ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝑑 ∈ V ) ) → ( 〈“ 𝐴 𝐵 𝑐 ”〉 = 〈“ 𝐴 𝐵 𝑑 ”〉 ↔ ( ( ♯ ‘ 〈“ 𝐴 𝐵 𝑐 ”〉 ) = 3 ∧ ( ( 〈“ 𝐴 𝐵 𝑐 ”〉 ‘ 0 ) = 𝐴 ∧ ( 〈“ 𝐴 𝐵 𝑐 ”〉 ‘ 1 ) = 𝐵 ∧ ( 〈“ 𝐴 𝐵 𝑐 ”〉 ‘ 2 ) = 𝑑 ) ) ) ) |
13 |
3 11 12
|
sylancr |
⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ∧ ( 𝑐 ∈ 𝑍 ∧ 𝑑 ∈ 𝑍 ) ) → ( 〈“ 𝐴 𝐵 𝑐 ”〉 = 〈“ 𝐴 𝐵 𝑑 ”〉 ↔ ( ( ♯ ‘ 〈“ 𝐴 𝐵 𝑐 ”〉 ) = 3 ∧ ( ( 〈“ 𝐴 𝐵 𝑐 ”〉 ‘ 0 ) = 𝐴 ∧ ( 〈“ 𝐴 𝐵 𝑐 ”〉 ‘ 1 ) = 𝐵 ∧ ( 〈“ 𝐴 𝐵 𝑐 ”〉 ‘ 2 ) = 𝑑 ) ) ) ) |
14 |
|
s3fv2 |
⊢ ( 𝑐 ∈ V → ( 〈“ 𝐴 𝐵 𝑐 ”〉 ‘ 2 ) = 𝑐 ) |
15 |
14
|
elv |
⊢ ( 〈“ 𝐴 𝐵 𝑐 ”〉 ‘ 2 ) = 𝑐 |
16 |
|
simp3 |
⊢ ( ( ( 〈“ 𝐴 𝐵 𝑐 ”〉 ‘ 0 ) = 𝐴 ∧ ( 〈“ 𝐴 𝐵 𝑐 ”〉 ‘ 1 ) = 𝐵 ∧ ( 〈“ 𝐴 𝐵 𝑐 ”〉 ‘ 2 ) = 𝑑 ) → ( 〈“ 𝐴 𝐵 𝑐 ”〉 ‘ 2 ) = 𝑑 ) |
17 |
15 16
|
syl5eqr |
⊢ ( ( ( 〈“ 𝐴 𝐵 𝑐 ”〉 ‘ 0 ) = 𝐴 ∧ ( 〈“ 𝐴 𝐵 𝑐 ”〉 ‘ 1 ) = 𝐵 ∧ ( 〈“ 𝐴 𝐵 𝑐 ”〉 ‘ 2 ) = 𝑑 ) → 𝑐 = 𝑑 ) |
18 |
17
|
adantl |
⊢ ( ( ( ♯ ‘ 〈“ 𝐴 𝐵 𝑐 ”〉 ) = 3 ∧ ( ( 〈“ 𝐴 𝐵 𝑐 ”〉 ‘ 0 ) = 𝐴 ∧ ( 〈“ 𝐴 𝐵 𝑐 ”〉 ‘ 1 ) = 𝐵 ∧ ( 〈“ 𝐴 𝐵 𝑐 ”〉 ‘ 2 ) = 𝑑 ) ) → 𝑐 = 𝑑 ) |
19 |
13 18
|
syl6bi |
⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ∧ ( 𝑐 ∈ 𝑍 ∧ 𝑑 ∈ 𝑍 ) ) → ( 〈“ 𝐴 𝐵 𝑐 ”〉 = 〈“ 𝐴 𝐵 𝑑 ”〉 → 𝑐 = 𝑑 ) ) |
20 |
19
|
con3rr3 |
⊢ ( ¬ 𝑐 = 𝑑 → ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ∧ ( 𝑐 ∈ 𝑍 ∧ 𝑑 ∈ 𝑍 ) ) → ¬ 〈“ 𝐴 𝐵 𝑐 ”〉 = 〈“ 𝐴 𝐵 𝑑 ”〉 ) ) |
21 |
20
|
imp |
⊢ ( ( ¬ 𝑐 = 𝑑 ∧ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ∧ ( 𝑐 ∈ 𝑍 ∧ 𝑑 ∈ 𝑍 ) ) ) → ¬ 〈“ 𝐴 𝐵 𝑐 ”〉 = 〈“ 𝐴 𝐵 𝑑 ”〉 ) |
22 |
21
|
neqned |
⊢ ( ( ¬ 𝑐 = 𝑑 ∧ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ∧ ( 𝑐 ∈ 𝑍 ∧ 𝑑 ∈ 𝑍 ) ) ) → 〈“ 𝐴 𝐵 𝑐 ”〉 ≠ 〈“ 𝐴 𝐵 𝑑 ”〉 ) |
23 |
|
disjsn2 |
⊢ ( 〈“ 𝐴 𝐵 𝑐 ”〉 ≠ 〈“ 𝐴 𝐵 𝑑 ”〉 → ( { 〈“ 𝐴 𝐵 𝑐 ”〉 } ∩ { 〈“ 𝐴 𝐵 𝑑 ”〉 } ) = ∅ ) |
24 |
22 23
|
syl |
⊢ ( ( ¬ 𝑐 = 𝑑 ∧ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ∧ ( 𝑐 ∈ 𝑍 ∧ 𝑑 ∈ 𝑍 ) ) ) → ( { 〈“ 𝐴 𝐵 𝑐 ”〉 } ∩ { 〈“ 𝐴 𝐵 𝑑 ”〉 } ) = ∅ ) |
25 |
24
|
olcd |
⊢ ( ( ¬ 𝑐 = 𝑑 ∧ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ∧ ( 𝑐 ∈ 𝑍 ∧ 𝑑 ∈ 𝑍 ) ) ) → ( 𝑐 = 𝑑 ∨ ( { 〈“ 𝐴 𝐵 𝑐 ”〉 } ∩ { 〈“ 𝐴 𝐵 𝑑 ”〉 } ) = ∅ ) ) |
26 |
25
|
ex |
⊢ ( ¬ 𝑐 = 𝑑 → ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ∧ ( 𝑐 ∈ 𝑍 ∧ 𝑑 ∈ 𝑍 ) ) → ( 𝑐 = 𝑑 ∨ ( { 〈“ 𝐴 𝐵 𝑐 ”〉 } ∩ { 〈“ 𝐴 𝐵 𝑑 ”〉 } ) = ∅ ) ) ) |
27 |
2 26
|
pm2.61i |
⊢ ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ∧ ( 𝑐 ∈ 𝑍 ∧ 𝑑 ∈ 𝑍 ) ) → ( 𝑐 = 𝑑 ∨ ( { 〈“ 𝐴 𝐵 𝑐 ”〉 } ∩ { 〈“ 𝐴 𝐵 𝑑 ”〉 } ) = ∅ ) ) |
28 |
27
|
ralrimivva |
⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) → ∀ 𝑐 ∈ 𝑍 ∀ 𝑑 ∈ 𝑍 ( 𝑐 = 𝑑 ∨ ( { 〈“ 𝐴 𝐵 𝑐 ”〉 } ∩ { 〈“ 𝐴 𝐵 𝑑 ”〉 } ) = ∅ ) ) |
29 |
|
eqidd |
⊢ ( 𝑐 = 𝑑 → 𝐴 = 𝐴 ) |
30 |
|
eqidd |
⊢ ( 𝑐 = 𝑑 → 𝐵 = 𝐵 ) |
31 |
|
id |
⊢ ( 𝑐 = 𝑑 → 𝑐 = 𝑑 ) |
32 |
29 30 31
|
s3eqd |
⊢ ( 𝑐 = 𝑑 → 〈“ 𝐴 𝐵 𝑐 ”〉 = 〈“ 𝐴 𝐵 𝑑 ”〉 ) |
33 |
32
|
sneqd |
⊢ ( 𝑐 = 𝑑 → { 〈“ 𝐴 𝐵 𝑐 ”〉 } = { 〈“ 𝐴 𝐵 𝑑 ”〉 } ) |
34 |
33
|
disjor |
⊢ ( Disj 𝑐 ∈ 𝑍 { 〈“ 𝐴 𝐵 𝑐 ”〉 } ↔ ∀ 𝑐 ∈ 𝑍 ∀ 𝑑 ∈ 𝑍 ( 𝑐 = 𝑑 ∨ ( { 〈“ 𝐴 𝐵 𝑐 ”〉 } ∩ { 〈“ 𝐴 𝐵 𝑑 ”〉 } ) = ∅ ) ) |
35 |
28 34
|
sylibr |
⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) → Disj 𝑐 ∈ 𝑍 { 〈“ 𝐴 𝐵 𝑐 ”〉 } ) |