Step |
Hyp |
Ref |
Expression |
1 |
|
pmtr3ncom.t |
⊢ 𝑇 = ( pmTrsp ‘ 𝐷 ) |
2 |
|
hashge3el3dif |
⊢ ( ( 𝐷 ∈ 𝑉 ∧ 3 ≤ ( ♯ ‘ 𝐷 ) ) → ∃ 𝑥 ∈ 𝐷 ∃ 𝑦 ∈ 𝐷 ∃ 𝑧 ∈ 𝐷 ( 𝑥 ≠ 𝑦 ∧ 𝑥 ≠ 𝑧 ∧ 𝑦 ≠ 𝑧 ) ) |
3 |
|
simprl |
⊢ ( ( ( ( ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 ∈ 𝐷 ) ∧ ( 𝑥 ≠ 𝑦 ∧ 𝑥 ≠ 𝑧 ∧ 𝑦 ≠ 𝑧 ) ) ∧ ( 𝐷 ∈ 𝑉 ∧ 3 ≤ ( ♯ ‘ 𝐷 ) ) ) → 𝐷 ∈ 𝑉 ) |
4 |
|
prssi |
⊢ ( ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) → { 𝑥 , 𝑦 } ⊆ 𝐷 ) |
5 |
4
|
adantr |
⊢ ( ( ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 ∈ 𝐷 ) → { 𝑥 , 𝑦 } ⊆ 𝐷 ) |
6 |
5
|
ad2antrr |
⊢ ( ( ( ( ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 ∈ 𝐷 ) ∧ ( 𝑥 ≠ 𝑦 ∧ 𝑥 ≠ 𝑧 ∧ 𝑦 ≠ 𝑧 ) ) ∧ ( 𝐷 ∈ 𝑉 ∧ 3 ≤ ( ♯ ‘ 𝐷 ) ) ) → { 𝑥 , 𝑦 } ⊆ 𝐷 ) |
7 |
|
simplll |
⊢ ( ( ( ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 ∈ 𝐷 ) ∧ ( 𝑥 ≠ 𝑦 ∧ 𝑥 ≠ 𝑧 ∧ 𝑦 ≠ 𝑧 ) ) → 𝑥 ∈ 𝐷 ) |
8 |
|
simplr |
⊢ ( ( ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 ∈ 𝐷 ) → 𝑦 ∈ 𝐷 ) |
9 |
8
|
adantr |
⊢ ( ( ( ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 ∈ 𝐷 ) ∧ ( 𝑥 ≠ 𝑦 ∧ 𝑥 ≠ 𝑧 ∧ 𝑦 ≠ 𝑧 ) ) → 𝑦 ∈ 𝐷 ) |
10 |
|
simpr1 |
⊢ ( ( ( ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 ∈ 𝐷 ) ∧ ( 𝑥 ≠ 𝑦 ∧ 𝑥 ≠ 𝑧 ∧ 𝑦 ≠ 𝑧 ) ) → 𝑥 ≠ 𝑦 ) |
11 |
|
pr2nelem |
⊢ ( ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ∧ 𝑥 ≠ 𝑦 ) → { 𝑥 , 𝑦 } ≈ 2o ) |
12 |
7 9 10 11
|
syl3anc |
⊢ ( ( ( ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 ∈ 𝐷 ) ∧ ( 𝑥 ≠ 𝑦 ∧ 𝑥 ≠ 𝑧 ∧ 𝑦 ≠ 𝑧 ) ) → { 𝑥 , 𝑦 } ≈ 2o ) |
13 |
12
|
adantr |
⊢ ( ( ( ( ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 ∈ 𝐷 ) ∧ ( 𝑥 ≠ 𝑦 ∧ 𝑥 ≠ 𝑧 ∧ 𝑦 ≠ 𝑧 ) ) ∧ ( 𝐷 ∈ 𝑉 ∧ 3 ≤ ( ♯ ‘ 𝐷 ) ) ) → { 𝑥 , 𝑦 } ≈ 2o ) |
14 |
|
eqid |
⊢ ran 𝑇 = ran 𝑇 |
15 |
1 14
|
pmtrrn |
⊢ ( ( 𝐷 ∈ 𝑉 ∧ { 𝑥 , 𝑦 } ⊆ 𝐷 ∧ { 𝑥 , 𝑦 } ≈ 2o ) → ( 𝑇 ‘ { 𝑥 , 𝑦 } ) ∈ ran 𝑇 ) |
16 |
3 6 13 15
|
syl3anc |
⊢ ( ( ( ( ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 ∈ 𝐷 ) ∧ ( 𝑥 ≠ 𝑦 ∧ 𝑥 ≠ 𝑧 ∧ 𝑦 ≠ 𝑧 ) ) ∧ ( 𝐷 ∈ 𝑉 ∧ 3 ≤ ( ♯ ‘ 𝐷 ) ) ) → ( 𝑇 ‘ { 𝑥 , 𝑦 } ) ∈ ran 𝑇 ) |
17 |
|
prssi |
⊢ ( ( 𝑦 ∈ 𝐷 ∧ 𝑧 ∈ 𝐷 ) → { 𝑦 , 𝑧 } ⊆ 𝐷 ) |
18 |
17
|
ad5ant23 |
⊢ ( ( ( ( ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 ∈ 𝐷 ) ∧ ( 𝑥 ≠ 𝑦 ∧ 𝑥 ≠ 𝑧 ∧ 𝑦 ≠ 𝑧 ) ) ∧ ( 𝐷 ∈ 𝑉 ∧ 3 ≤ ( ♯ ‘ 𝐷 ) ) ) → { 𝑦 , 𝑧 } ⊆ 𝐷 ) |
19 |
|
simplr |
⊢ ( ( ( ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 ∈ 𝐷 ) ∧ ( 𝑥 ≠ 𝑦 ∧ 𝑥 ≠ 𝑧 ∧ 𝑦 ≠ 𝑧 ) ) → 𝑧 ∈ 𝐷 ) |
20 |
|
simpr3 |
⊢ ( ( ( ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 ∈ 𝐷 ) ∧ ( 𝑥 ≠ 𝑦 ∧ 𝑥 ≠ 𝑧 ∧ 𝑦 ≠ 𝑧 ) ) → 𝑦 ≠ 𝑧 ) |
21 |
|
pr2nelem |
⊢ ( ( 𝑦 ∈ 𝐷 ∧ 𝑧 ∈ 𝐷 ∧ 𝑦 ≠ 𝑧 ) → { 𝑦 , 𝑧 } ≈ 2o ) |
22 |
9 19 20 21
|
syl3anc |
⊢ ( ( ( ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 ∈ 𝐷 ) ∧ ( 𝑥 ≠ 𝑦 ∧ 𝑥 ≠ 𝑧 ∧ 𝑦 ≠ 𝑧 ) ) → { 𝑦 , 𝑧 } ≈ 2o ) |
23 |
22
|
adantr |
⊢ ( ( ( ( ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 ∈ 𝐷 ) ∧ ( 𝑥 ≠ 𝑦 ∧ 𝑥 ≠ 𝑧 ∧ 𝑦 ≠ 𝑧 ) ) ∧ ( 𝐷 ∈ 𝑉 ∧ 3 ≤ ( ♯ ‘ 𝐷 ) ) ) → { 𝑦 , 𝑧 } ≈ 2o ) |
24 |
1 14
|
pmtrrn |
⊢ ( ( 𝐷 ∈ 𝑉 ∧ { 𝑦 , 𝑧 } ⊆ 𝐷 ∧ { 𝑦 , 𝑧 } ≈ 2o ) → ( 𝑇 ‘ { 𝑦 , 𝑧 } ) ∈ ran 𝑇 ) |
25 |
3 18 23 24
|
syl3anc |
⊢ ( ( ( ( ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 ∈ 𝐷 ) ∧ ( 𝑥 ≠ 𝑦 ∧ 𝑥 ≠ 𝑧 ∧ 𝑦 ≠ 𝑧 ) ) ∧ ( 𝐷 ∈ 𝑉 ∧ 3 ≤ ( ♯ ‘ 𝐷 ) ) ) → ( 𝑇 ‘ { 𝑦 , 𝑧 } ) ∈ ran 𝑇 ) |
26 |
|
df-3an |
⊢ ( ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ∧ 𝑧 ∈ 𝐷 ) ↔ ( ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 ∈ 𝐷 ) ) |
27 |
26
|
biimpri |
⊢ ( ( ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 ∈ 𝐷 ) → ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ∧ 𝑧 ∈ 𝐷 ) ) |
28 |
27
|
ad2antrr |
⊢ ( ( ( ( ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 ∈ 𝐷 ) ∧ ( 𝑥 ≠ 𝑦 ∧ 𝑥 ≠ 𝑧 ∧ 𝑦 ≠ 𝑧 ) ) ∧ ( 𝐷 ∈ 𝑉 ∧ 3 ≤ ( ♯ ‘ 𝐷 ) ) ) → ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ∧ 𝑧 ∈ 𝐷 ) ) |
29 |
|
simplr |
⊢ ( ( ( ( ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 ∈ 𝐷 ) ∧ ( 𝑥 ≠ 𝑦 ∧ 𝑥 ≠ 𝑧 ∧ 𝑦 ≠ 𝑧 ) ) ∧ ( 𝐷 ∈ 𝑉 ∧ 3 ≤ ( ♯ ‘ 𝐷 ) ) ) → ( 𝑥 ≠ 𝑦 ∧ 𝑥 ≠ 𝑧 ∧ 𝑦 ≠ 𝑧 ) ) |
30 |
|
eqid |
⊢ ( 𝑇 ‘ { 𝑥 , 𝑦 } ) = ( 𝑇 ‘ { 𝑥 , 𝑦 } ) |
31 |
|
eqid |
⊢ ( 𝑇 ‘ { 𝑦 , 𝑧 } ) = ( 𝑇 ‘ { 𝑦 , 𝑧 } ) |
32 |
1 30 31
|
pmtr3ncomlem2 |
⊢ ( ( 𝐷 ∈ 𝑉 ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ∧ 𝑧 ∈ 𝐷 ) ∧ ( 𝑥 ≠ 𝑦 ∧ 𝑥 ≠ 𝑧 ∧ 𝑦 ≠ 𝑧 ) ) → ( ( 𝑇 ‘ { 𝑦 , 𝑧 } ) ∘ ( 𝑇 ‘ { 𝑥 , 𝑦 } ) ) ≠ ( ( 𝑇 ‘ { 𝑥 , 𝑦 } ) ∘ ( 𝑇 ‘ { 𝑦 , 𝑧 } ) ) ) |
33 |
3 28 29 32
|
syl3anc |
⊢ ( ( ( ( ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 ∈ 𝐷 ) ∧ ( 𝑥 ≠ 𝑦 ∧ 𝑥 ≠ 𝑧 ∧ 𝑦 ≠ 𝑧 ) ) ∧ ( 𝐷 ∈ 𝑉 ∧ 3 ≤ ( ♯ ‘ 𝐷 ) ) ) → ( ( 𝑇 ‘ { 𝑦 , 𝑧 } ) ∘ ( 𝑇 ‘ { 𝑥 , 𝑦 } ) ) ≠ ( ( 𝑇 ‘ { 𝑥 , 𝑦 } ) ∘ ( 𝑇 ‘ { 𝑦 , 𝑧 } ) ) ) |
34 |
|
coeq2 |
⊢ ( 𝑓 = ( 𝑇 ‘ { 𝑥 , 𝑦 } ) → ( 𝑔 ∘ 𝑓 ) = ( 𝑔 ∘ ( 𝑇 ‘ { 𝑥 , 𝑦 } ) ) ) |
35 |
|
coeq1 |
⊢ ( 𝑓 = ( 𝑇 ‘ { 𝑥 , 𝑦 } ) → ( 𝑓 ∘ 𝑔 ) = ( ( 𝑇 ‘ { 𝑥 , 𝑦 } ) ∘ 𝑔 ) ) |
36 |
34 35
|
neeq12d |
⊢ ( 𝑓 = ( 𝑇 ‘ { 𝑥 , 𝑦 } ) → ( ( 𝑔 ∘ 𝑓 ) ≠ ( 𝑓 ∘ 𝑔 ) ↔ ( 𝑔 ∘ ( 𝑇 ‘ { 𝑥 , 𝑦 } ) ) ≠ ( ( 𝑇 ‘ { 𝑥 , 𝑦 } ) ∘ 𝑔 ) ) ) |
37 |
|
coeq1 |
⊢ ( 𝑔 = ( 𝑇 ‘ { 𝑦 , 𝑧 } ) → ( 𝑔 ∘ ( 𝑇 ‘ { 𝑥 , 𝑦 } ) ) = ( ( 𝑇 ‘ { 𝑦 , 𝑧 } ) ∘ ( 𝑇 ‘ { 𝑥 , 𝑦 } ) ) ) |
38 |
|
coeq2 |
⊢ ( 𝑔 = ( 𝑇 ‘ { 𝑦 , 𝑧 } ) → ( ( 𝑇 ‘ { 𝑥 , 𝑦 } ) ∘ 𝑔 ) = ( ( 𝑇 ‘ { 𝑥 , 𝑦 } ) ∘ ( 𝑇 ‘ { 𝑦 , 𝑧 } ) ) ) |
39 |
37 38
|
neeq12d |
⊢ ( 𝑔 = ( 𝑇 ‘ { 𝑦 , 𝑧 } ) → ( ( 𝑔 ∘ ( 𝑇 ‘ { 𝑥 , 𝑦 } ) ) ≠ ( ( 𝑇 ‘ { 𝑥 , 𝑦 } ) ∘ 𝑔 ) ↔ ( ( 𝑇 ‘ { 𝑦 , 𝑧 } ) ∘ ( 𝑇 ‘ { 𝑥 , 𝑦 } ) ) ≠ ( ( 𝑇 ‘ { 𝑥 , 𝑦 } ) ∘ ( 𝑇 ‘ { 𝑦 , 𝑧 } ) ) ) ) |
40 |
36 39
|
rspc2ev |
⊢ ( ( ( 𝑇 ‘ { 𝑥 , 𝑦 } ) ∈ ran 𝑇 ∧ ( 𝑇 ‘ { 𝑦 , 𝑧 } ) ∈ ran 𝑇 ∧ ( ( 𝑇 ‘ { 𝑦 , 𝑧 } ) ∘ ( 𝑇 ‘ { 𝑥 , 𝑦 } ) ) ≠ ( ( 𝑇 ‘ { 𝑥 , 𝑦 } ) ∘ ( 𝑇 ‘ { 𝑦 , 𝑧 } ) ) ) → ∃ 𝑓 ∈ ran 𝑇 ∃ 𝑔 ∈ ran 𝑇 ( 𝑔 ∘ 𝑓 ) ≠ ( 𝑓 ∘ 𝑔 ) ) |
41 |
16 25 33 40
|
syl3anc |
⊢ ( ( ( ( ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 ∈ 𝐷 ) ∧ ( 𝑥 ≠ 𝑦 ∧ 𝑥 ≠ 𝑧 ∧ 𝑦 ≠ 𝑧 ) ) ∧ ( 𝐷 ∈ 𝑉 ∧ 3 ≤ ( ♯ ‘ 𝐷 ) ) ) → ∃ 𝑓 ∈ ran 𝑇 ∃ 𝑔 ∈ ran 𝑇 ( 𝑔 ∘ 𝑓 ) ≠ ( 𝑓 ∘ 𝑔 ) ) |
42 |
41
|
exp31 |
⊢ ( ( ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ∧ 𝑧 ∈ 𝐷 ) → ( ( 𝑥 ≠ 𝑦 ∧ 𝑥 ≠ 𝑧 ∧ 𝑦 ≠ 𝑧 ) → ( ( 𝐷 ∈ 𝑉 ∧ 3 ≤ ( ♯ ‘ 𝐷 ) ) → ∃ 𝑓 ∈ ran 𝑇 ∃ 𝑔 ∈ ran 𝑇 ( 𝑔 ∘ 𝑓 ) ≠ ( 𝑓 ∘ 𝑔 ) ) ) ) |
43 |
42
|
rexlimdva |
⊢ ( ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) → ( ∃ 𝑧 ∈ 𝐷 ( 𝑥 ≠ 𝑦 ∧ 𝑥 ≠ 𝑧 ∧ 𝑦 ≠ 𝑧 ) → ( ( 𝐷 ∈ 𝑉 ∧ 3 ≤ ( ♯ ‘ 𝐷 ) ) → ∃ 𝑓 ∈ ran 𝑇 ∃ 𝑔 ∈ ran 𝑇 ( 𝑔 ∘ 𝑓 ) ≠ ( 𝑓 ∘ 𝑔 ) ) ) ) |
44 |
43
|
rexlimivv |
⊢ ( ∃ 𝑥 ∈ 𝐷 ∃ 𝑦 ∈ 𝐷 ∃ 𝑧 ∈ 𝐷 ( 𝑥 ≠ 𝑦 ∧ 𝑥 ≠ 𝑧 ∧ 𝑦 ≠ 𝑧 ) → ( ( 𝐷 ∈ 𝑉 ∧ 3 ≤ ( ♯ ‘ 𝐷 ) ) → ∃ 𝑓 ∈ ran 𝑇 ∃ 𝑔 ∈ ran 𝑇 ( 𝑔 ∘ 𝑓 ) ≠ ( 𝑓 ∘ 𝑔 ) ) ) |
45 |
2 44
|
mpcom |
⊢ ( ( 𝐷 ∈ 𝑉 ∧ 3 ≤ ( ♯ ‘ 𝐷 ) ) → ∃ 𝑓 ∈ ran 𝑇 ∃ 𝑔 ∈ ran 𝑇 ( 𝑔 ∘ 𝑓 ) ≠ ( 𝑓 ∘ 𝑔 ) ) |