Step |
Hyp |
Ref |
Expression |
1 |
|
snidg |
⊢ ( 𝑋 ∈ 𝑉 → 𝑋 ∈ { 𝑋 } ) |
2 |
1
|
anim1i |
⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) → ( 𝑋 ∈ { 𝑋 } ∧ 𝑌 ∈ 𝐴 ) ) |
3 |
|
eqid |
⊢ 𝑌 = 𝑌 |
4 |
2 3
|
jctir |
⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) → ( ( 𝑋 ∈ { 𝑋 } ∧ 𝑌 ∈ 𝐴 ) ∧ 𝑌 = 𝑌 ) ) |
5 |
|
2ndconst |
⊢ ( 𝑋 ∈ 𝑉 → ( 2nd ↾ ( { 𝑋 } × 𝐴 ) ) : ( { 𝑋 } × 𝐴 ) –1-1-onto→ 𝐴 ) |
6 |
5
|
adantr |
⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) → ( 2nd ↾ ( { 𝑋 } × 𝐴 ) ) : ( { 𝑋 } × 𝐴 ) –1-1-onto→ 𝐴 ) |
7 |
|
f1ocnv |
⊢ ( ( 2nd ↾ ( { 𝑋 } × 𝐴 ) ) : ( { 𝑋 } × 𝐴 ) –1-1-onto→ 𝐴 → ◡ ( 2nd ↾ ( { 𝑋 } × 𝐴 ) ) : 𝐴 –1-1-onto→ ( { 𝑋 } × 𝐴 ) ) |
8 |
|
f1ofn |
⊢ ( ◡ ( 2nd ↾ ( { 𝑋 } × 𝐴 ) ) : 𝐴 –1-1-onto→ ( { 𝑋 } × 𝐴 ) → ◡ ( 2nd ↾ ( { 𝑋 } × 𝐴 ) ) Fn 𝐴 ) |
9 |
6 7 8
|
3syl |
⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) → ◡ ( 2nd ↾ ( { 𝑋 } × 𝐴 ) ) Fn 𝐴 ) |
10 |
|
fnbrfvb |
⊢ ( ( ◡ ( 2nd ↾ ( { 𝑋 } × 𝐴 ) ) Fn 𝐴 ∧ 𝑌 ∈ 𝐴 ) → ( ( ◡ ( 2nd ↾ ( { 𝑋 } × 𝐴 ) ) ‘ 𝑌 ) = 〈 𝑋 , 𝑌 〉 ↔ 𝑌 ◡ ( 2nd ↾ ( { 𝑋 } × 𝐴 ) ) 〈 𝑋 , 𝑌 〉 ) ) |
11 |
9 10
|
sylancom |
⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) → ( ( ◡ ( 2nd ↾ ( { 𝑋 } × 𝐴 ) ) ‘ 𝑌 ) = 〈 𝑋 , 𝑌 〉 ↔ 𝑌 ◡ ( 2nd ↾ ( { 𝑋 } × 𝐴 ) ) 〈 𝑋 , 𝑌 〉 ) ) |
12 |
|
opex |
⊢ 〈 𝑋 , 𝑌 〉 ∈ V |
13 |
|
brcnvg |
⊢ ( ( 𝑌 ∈ 𝐴 ∧ 〈 𝑋 , 𝑌 〉 ∈ V ) → ( 𝑌 ◡ ( 2nd ↾ ( { 𝑋 } × 𝐴 ) ) 〈 𝑋 , 𝑌 〉 ↔ 〈 𝑋 , 𝑌 〉 ( 2nd ↾ ( { 𝑋 } × 𝐴 ) ) 𝑌 ) ) |
14 |
12 13
|
mpan2 |
⊢ ( 𝑌 ∈ 𝐴 → ( 𝑌 ◡ ( 2nd ↾ ( { 𝑋 } × 𝐴 ) ) 〈 𝑋 , 𝑌 〉 ↔ 〈 𝑋 , 𝑌 〉 ( 2nd ↾ ( { 𝑋 } × 𝐴 ) ) 𝑌 ) ) |
15 |
14
|
adantl |
⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) → ( 𝑌 ◡ ( 2nd ↾ ( { 𝑋 } × 𝐴 ) ) 〈 𝑋 , 𝑌 〉 ↔ 〈 𝑋 , 𝑌 〉 ( 2nd ↾ ( { 𝑋 } × 𝐴 ) ) 𝑌 ) ) |
16 |
|
brres |
⊢ ( 𝑌 ∈ 𝐴 → ( 〈 𝑋 , 𝑌 〉 ( 2nd ↾ ( { 𝑋 } × 𝐴 ) ) 𝑌 ↔ ( 〈 𝑋 , 𝑌 〉 ∈ ( { 𝑋 } × 𝐴 ) ∧ 〈 𝑋 , 𝑌 〉 2nd 𝑌 ) ) ) |
17 |
16
|
adantl |
⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) → ( 〈 𝑋 , 𝑌 〉 ( 2nd ↾ ( { 𝑋 } × 𝐴 ) ) 𝑌 ↔ ( 〈 𝑋 , 𝑌 〉 ∈ ( { 𝑋 } × 𝐴 ) ∧ 〈 𝑋 , 𝑌 〉 2nd 𝑌 ) ) ) |
18 |
|
opelxp |
⊢ ( 〈 𝑋 , 𝑌 〉 ∈ ( { 𝑋 } × 𝐴 ) ↔ ( 𝑋 ∈ { 𝑋 } ∧ 𝑌 ∈ 𝐴 ) ) |
19 |
18
|
anbi1i |
⊢ ( ( 〈 𝑋 , 𝑌 〉 ∈ ( { 𝑋 } × 𝐴 ) ∧ 〈 𝑋 , 𝑌 〉 2nd 𝑌 ) ↔ ( ( 𝑋 ∈ { 𝑋 } ∧ 𝑌 ∈ 𝐴 ) ∧ 〈 𝑋 , 𝑌 〉 2nd 𝑌 ) ) |
20 |
|
br2ndeqg |
⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) → ( 〈 𝑋 , 𝑌 〉 2nd 𝑌 ↔ 𝑌 = 𝑌 ) ) |
21 |
20
|
anbi2d |
⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) → ( ( ( 𝑋 ∈ { 𝑋 } ∧ 𝑌 ∈ 𝐴 ) ∧ 〈 𝑋 , 𝑌 〉 2nd 𝑌 ) ↔ ( ( 𝑋 ∈ { 𝑋 } ∧ 𝑌 ∈ 𝐴 ) ∧ 𝑌 = 𝑌 ) ) ) |
22 |
19 21
|
syl5bb |
⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) → ( ( 〈 𝑋 , 𝑌 〉 ∈ ( { 𝑋 } × 𝐴 ) ∧ 〈 𝑋 , 𝑌 〉 2nd 𝑌 ) ↔ ( ( 𝑋 ∈ { 𝑋 } ∧ 𝑌 ∈ 𝐴 ) ∧ 𝑌 = 𝑌 ) ) ) |
23 |
17 22
|
bitrd |
⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) → ( 〈 𝑋 , 𝑌 〉 ( 2nd ↾ ( { 𝑋 } × 𝐴 ) ) 𝑌 ↔ ( ( 𝑋 ∈ { 𝑋 } ∧ 𝑌 ∈ 𝐴 ) ∧ 𝑌 = 𝑌 ) ) ) |
24 |
15 23
|
bitrd |
⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) → ( 𝑌 ◡ ( 2nd ↾ ( { 𝑋 } × 𝐴 ) ) 〈 𝑋 , 𝑌 〉 ↔ ( ( 𝑋 ∈ { 𝑋 } ∧ 𝑌 ∈ 𝐴 ) ∧ 𝑌 = 𝑌 ) ) ) |
25 |
11 24
|
bitrd |
⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) → ( ( ◡ ( 2nd ↾ ( { 𝑋 } × 𝐴 ) ) ‘ 𝑌 ) = 〈 𝑋 , 𝑌 〉 ↔ ( ( 𝑋 ∈ { 𝑋 } ∧ 𝑌 ∈ 𝐴 ) ∧ 𝑌 = 𝑌 ) ) ) |
26 |
4 25
|
mpbird |
⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴 ) → ( ◡ ( 2nd ↾ ( { 𝑋 } × 𝐴 ) ) ‘ 𝑌 ) = 〈 𝑋 , 𝑌 〉 ) |