Proof of Theorem fv2ndcnv
Step | Hyp | Ref
| Expression |
1 | | snidg 4560 |
. . . 4
⊢ (𝑋 ∈ 𝑉 → 𝑋 ∈ {𝑋}) |
2 | 1 | anim1i 618 |
. . 3
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴) → (𝑋 ∈ {𝑋} ∧ 𝑌 ∈ 𝐴)) |
3 | | eqid 2739 |
. . 3
⊢ 𝑌 = 𝑌 |
4 | 2, 3 | jctir 524 |
. 2
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴) → ((𝑋 ∈ {𝑋} ∧ 𝑌 ∈ 𝐴) ∧ 𝑌 = 𝑌)) |
5 | | 2ndconst 7835 |
. . . . . 6
⊢ (𝑋 ∈ 𝑉 → (2nd ↾ ({𝑋} × 𝐴)):({𝑋} × 𝐴)–1-1-onto→𝐴) |
6 | 5 | adantr 484 |
. . . . 5
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴) → (2nd ↾ ({𝑋} × 𝐴)):({𝑋} × 𝐴)–1-1-onto→𝐴) |
7 | | f1ocnv 6643 |
. . . . 5
⊢
((2nd ↾ ({𝑋} × 𝐴)):({𝑋} × 𝐴)–1-1-onto→𝐴 → ◡(2nd ↾ ({𝑋} × 𝐴)):𝐴–1-1-onto→({𝑋} × 𝐴)) |
8 | | f1ofn 6632 |
. . . . 5
⊢ (◡(2nd ↾ ({𝑋} × 𝐴)):𝐴–1-1-onto→({𝑋} × 𝐴) → ◡(2nd ↾ ({𝑋} × 𝐴)) Fn 𝐴) |
9 | 6, 7, 8 | 3syl 18 |
. . . 4
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴) → ◡(2nd ↾ ({𝑋} × 𝐴)) Fn 𝐴) |
10 | | fnbrfvb 6735 |
. . . 4
⊢ ((◡(2nd ↾ ({𝑋} × 𝐴)) Fn 𝐴 ∧ 𝑌 ∈ 𝐴) → ((◡(2nd ↾ ({𝑋} × 𝐴))‘𝑌) = 〈𝑋, 𝑌〉 ↔ 𝑌◡(2nd ↾ ({𝑋} × 𝐴))〈𝑋, 𝑌〉)) |
11 | 9, 10 | sylancom 591 |
. . 3
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴) → ((◡(2nd ↾ ({𝑋} × 𝐴))‘𝑌) = 〈𝑋, 𝑌〉 ↔ 𝑌◡(2nd ↾ ({𝑋} × 𝐴))〈𝑋, 𝑌〉)) |
12 | | opex 5332 |
. . . . . 6
⊢
〈𝑋, 𝑌〉 ∈ V |
13 | | brcnvg 5732 |
. . . . . 6
⊢ ((𝑌 ∈ 𝐴 ∧ 〈𝑋, 𝑌〉 ∈ V) → (𝑌◡(2nd ↾ ({𝑋} × 𝐴))〈𝑋, 𝑌〉 ↔ 〈𝑋, 𝑌〉(2nd ↾ ({𝑋} × 𝐴))𝑌)) |
14 | 12, 13 | mpan2 691 |
. . . . 5
⊢ (𝑌 ∈ 𝐴 → (𝑌◡(2nd ↾ ({𝑋} × 𝐴))〈𝑋, 𝑌〉 ↔ 〈𝑋, 𝑌〉(2nd ↾ ({𝑋} × 𝐴))𝑌)) |
15 | 14 | adantl 485 |
. . . 4
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴) → (𝑌◡(2nd ↾ ({𝑋} × 𝐴))〈𝑋, 𝑌〉 ↔ 〈𝑋, 𝑌〉(2nd ↾ ({𝑋} × 𝐴))𝑌)) |
16 | | brres 5842 |
. . . . . 6
⊢ (𝑌 ∈ 𝐴 → (〈𝑋, 𝑌〉(2nd ↾ ({𝑋} × 𝐴))𝑌 ↔ (〈𝑋, 𝑌〉 ∈ ({𝑋} × 𝐴) ∧ 〈𝑋, 𝑌〉2nd 𝑌))) |
17 | 16 | adantl 485 |
. . . . 5
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴) → (〈𝑋, 𝑌〉(2nd ↾ ({𝑋} × 𝐴))𝑌 ↔ (〈𝑋, 𝑌〉 ∈ ({𝑋} × 𝐴) ∧ 〈𝑋, 𝑌〉2nd 𝑌))) |
18 | | opelxp 5571 |
. . . . . . 7
⊢
(〈𝑋, 𝑌〉 ∈ ({𝑋} × 𝐴) ↔ (𝑋 ∈ {𝑋} ∧ 𝑌 ∈ 𝐴)) |
19 | 18 | anbi1i 627 |
. . . . . 6
⊢
((〈𝑋, 𝑌〉 ∈ ({𝑋} × 𝐴) ∧ 〈𝑋, 𝑌〉2nd 𝑌) ↔ ((𝑋 ∈ {𝑋} ∧ 𝑌 ∈ 𝐴) ∧ 〈𝑋, 𝑌〉2nd 𝑌)) |
20 | | br2ndeqg 7750 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴) → (〈𝑋, 𝑌〉2nd 𝑌 ↔ 𝑌 = 𝑌)) |
21 | 20 | anbi2d 632 |
. . . . . 6
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴) → (((𝑋 ∈ {𝑋} ∧ 𝑌 ∈ 𝐴) ∧ 〈𝑋, 𝑌〉2nd 𝑌) ↔ ((𝑋 ∈ {𝑋} ∧ 𝑌 ∈ 𝐴) ∧ 𝑌 = 𝑌))) |
22 | 19, 21 | syl5bb 286 |
. . . . 5
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴) → ((〈𝑋, 𝑌〉 ∈ ({𝑋} × 𝐴) ∧ 〈𝑋, 𝑌〉2nd 𝑌) ↔ ((𝑋 ∈ {𝑋} ∧ 𝑌 ∈ 𝐴) ∧ 𝑌 = 𝑌))) |
23 | 17, 22 | bitrd 282 |
. . . 4
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴) → (〈𝑋, 𝑌〉(2nd ↾ ({𝑋} × 𝐴))𝑌 ↔ ((𝑋 ∈ {𝑋} ∧ 𝑌 ∈ 𝐴) ∧ 𝑌 = 𝑌))) |
24 | 15, 23 | bitrd 282 |
. . 3
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴) → (𝑌◡(2nd ↾ ({𝑋} × 𝐴))〈𝑋, 𝑌〉 ↔ ((𝑋 ∈ {𝑋} ∧ 𝑌 ∈ 𝐴) ∧ 𝑌 = 𝑌))) |
25 | 11, 24 | bitrd 282 |
. 2
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴) → ((◡(2nd ↾ ({𝑋} × 𝐴))‘𝑌) = 〈𝑋, 𝑌〉 ↔ ((𝑋 ∈ {𝑋} ∧ 𝑌 ∈ 𝐴) ∧ 𝑌 = 𝑌))) |
26 | 4, 25 | mpbird 260 |
1
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴) → (◡(2nd ↾ ({𝑋} × 𝐴))‘𝑌) = 〈𝑋, 𝑌〉) |