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