Step |
Hyp |
Ref |
Expression |
1 |
|
c0ex |
⊢ 0 ∈ V |
2 |
|
1ex |
⊢ 1 ∈ V |
3 |
|
2ex |
⊢ 2 ∈ V |
4 |
1 2 3
|
3pm3.2i |
⊢ ( 0 ∈ V ∧ 1 ∈ V ∧ 2 ∈ V ) |
5 |
4
|
a1i |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( 0 ∈ V ∧ 1 ∈ V ∧ 2 ∈ V ) ) |
6 |
|
funcnvtp |
⊢ ( ( ( 0 ∈ V ∧ 1 ∈ V ∧ 2 ∈ V ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) → Fun ◡ { 〈 0 , 𝐴 〉 , 〈 1 , 𝐵 〉 , 〈 2 , 𝐶 〉 } ) |
7 |
5 6
|
sylan |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) → Fun ◡ { 〈 0 , 𝐴 〉 , 〈 1 , 𝐵 〉 , 〈 2 , 𝐶 〉 } ) |
8 |
|
s3tpop |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → 〈“ 𝐴 𝐵 𝐶 ”〉 = { 〈 0 , 𝐴 〉 , 〈 1 , 𝐵 〉 , 〈 2 , 𝐶 〉 } ) |
9 |
8
|
adantr |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) → 〈“ 𝐴 𝐵 𝐶 ”〉 = { 〈 0 , 𝐴 〉 , 〈 1 , 𝐵 〉 , 〈 2 , 𝐶 〉 } ) |
10 |
9
|
cnveqd |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) → ◡ 〈“ 𝐴 𝐵 𝐶 ”〉 = ◡ { 〈 0 , 𝐴 〉 , 〈 1 , 𝐵 〉 , 〈 2 , 𝐶 〉 } ) |
11 |
10
|
funeqd |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) → ( Fun ◡ 〈“ 𝐴 𝐵 𝐶 ”〉 ↔ Fun ◡ { 〈 0 , 𝐴 〉 , 〈 1 , 𝐵 〉 , 〈 2 , 𝐶 〉 } ) ) |
12 |
7 11
|
mpbird |
⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ∧ ( 𝐴 ≠ 𝐵 ∧ 𝐴 ≠ 𝐶 ∧ 𝐵 ≠ 𝐶 ) ) → Fun ◡ 〈“ 𝐴 𝐵 𝐶 ”〉 ) |