Proof of Theorem fv2ndcnv
Step | Hyp | Ref
| Expression |
1 | | snidg 4206 |
. . . 4
⊢ (𝑋 ∈ 𝑉 → 𝑋 ∈ {𝑋}) |
2 | 1 | anim1i 592 |
. . 3
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴) → (𝑋 ∈ {𝑋} ∧ 𝑌 ∈ 𝐴)) |
3 | | eqid 2622 |
. . 3
⊢ 𝑌 = 𝑌 |
4 | 2, 3 | jctil 560 |
. 2
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴) → (𝑌 = 𝑌 ∧ (𝑋 ∈ {𝑋} ∧ 𝑌 ∈ 𝐴))) |
5 | | 2ndconst 7266 |
. . . . . 6
⊢ (𝑋 ∈ 𝑉 → (2nd ↾ ({𝑋} × 𝐴)):({𝑋} × 𝐴)–1-1-onto→𝐴) |
6 | 5 | adantr 481 |
. . . . 5
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴) → (2nd ↾ ({𝑋} × 𝐴)):({𝑋} × 𝐴)–1-1-onto→𝐴) |
7 | | f1ocnv 6149 |
. . . . 5
⊢
((2nd ↾ ({𝑋} × 𝐴)):({𝑋} × 𝐴)–1-1-onto→𝐴 → ◡(2nd ↾ ({𝑋} × 𝐴)):𝐴–1-1-onto→({𝑋} × 𝐴)) |
8 | | f1ofn 6138 |
. . . . 5
⊢ (◡(2nd ↾ ({𝑋} × 𝐴)):𝐴–1-1-onto→({𝑋} × 𝐴) → ◡(2nd ↾ ({𝑋} × 𝐴)) Fn 𝐴) |
9 | 6, 7, 8 | 3syl 18 |
. . . 4
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴) → ◡(2nd ↾ ({𝑋} × 𝐴)) Fn 𝐴) |
10 | | fnbrfvb 6236 |
. . . 4
⊢ ((◡(2nd ↾ ({𝑋} × 𝐴)) Fn 𝐴 ∧ 𝑌 ∈ 𝐴) → ((◡(2nd ↾ ({𝑋} × 𝐴))‘𝑌) = 〈𝑋, 𝑌〉 ↔ 𝑌◡(2nd ↾ ({𝑋} × 𝐴))〈𝑋, 𝑌〉)) |
11 | 9, 10 | sylancom 701 |
. . 3
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴) → ((◡(2nd ↾ ({𝑋} × 𝐴))‘𝑌) = 〈𝑋, 𝑌〉 ↔ 𝑌◡(2nd ↾ ({𝑋} × 𝐴))〈𝑋, 𝑌〉)) |
12 | | opex 4932 |
. . . . . 6
⊢
〈𝑋, 𝑌〉 ∈ V |
13 | | brcnvg 5303 |
. . . . . 6
⊢ ((𝑌 ∈ 𝐴 ∧ 〈𝑋, 𝑌〉 ∈ V) → (𝑌◡(2nd ↾ ({𝑋} × 𝐴))〈𝑋, 𝑌〉 ↔ 〈𝑋, 𝑌〉(2nd ↾ ({𝑋} × 𝐴))𝑌)) |
14 | 12, 13 | mpan2 707 |
. . . . 5
⊢ (𝑌 ∈ 𝐴 → (𝑌◡(2nd ↾ ({𝑋} × 𝐴))〈𝑋, 𝑌〉 ↔ 〈𝑋, 𝑌〉(2nd ↾ ({𝑋} × 𝐴))𝑌)) |
15 | 14 | adantl 482 |
. . . 4
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴) → (𝑌◡(2nd ↾ ({𝑋} × 𝐴))〈𝑋, 𝑌〉 ↔ 〈𝑋, 𝑌〉(2nd ↾ ({𝑋} × 𝐴))𝑌)) |
16 | | brresg 5405 |
. . . . . 6
⊢ (𝑌 ∈ 𝐴 → (〈𝑋, 𝑌〉(2nd ↾ ({𝑋} × 𝐴))𝑌 ↔ (〈𝑋, 𝑌〉2nd 𝑌 ∧ 〈𝑋, 𝑌〉 ∈ ({𝑋} × 𝐴)))) |
17 | 16 | adantl 482 |
. . . . 5
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴) → (〈𝑋, 𝑌〉(2nd ↾ ({𝑋} × 𝐴))𝑌 ↔ (〈𝑋, 𝑌〉2nd 𝑌 ∧ 〈𝑋, 𝑌〉 ∈ ({𝑋} × 𝐴)))) |
18 | | opelxp 5146 |
. . . . . . 7
⊢
(〈𝑋, 𝑌〉 ∈ ({𝑋} × 𝐴) ↔ (𝑋 ∈ {𝑋} ∧ 𝑌 ∈ 𝐴)) |
19 | 18 | anbi2i 730 |
. . . . . 6
⊢
((〈𝑋, 𝑌〉2nd 𝑌 ∧ 〈𝑋, 𝑌〉 ∈ ({𝑋} × 𝐴)) ↔ (〈𝑋, 𝑌〉2nd 𝑌 ∧ (𝑋 ∈ {𝑋} ∧ 𝑌 ∈ 𝐴))) |
20 | | br2ndeqg 31673 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴) → (〈𝑋, 𝑌〉2nd 𝑌 ↔ 𝑌 = 𝑌)) |
21 | 20 | anbi1d 741 |
. . . . . 6
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴) → ((〈𝑋, 𝑌〉2nd 𝑌 ∧ (𝑋 ∈ {𝑋} ∧ 𝑌 ∈ 𝐴)) ↔ (𝑌 = 𝑌 ∧ (𝑋 ∈ {𝑋} ∧ 𝑌 ∈ 𝐴)))) |
22 | 19, 21 | syl5bb 272 |
. . . . 5
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴) → ((〈𝑋, 𝑌〉2nd 𝑌 ∧ 〈𝑋, 𝑌〉 ∈ ({𝑋} × 𝐴)) ↔ (𝑌 = 𝑌 ∧ (𝑋 ∈ {𝑋} ∧ 𝑌 ∈ 𝐴)))) |
23 | 17, 22 | bitrd 268 |
. . . 4
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴) → (〈𝑋, 𝑌〉(2nd ↾ ({𝑋} × 𝐴))𝑌 ↔ (𝑌 = 𝑌 ∧ (𝑋 ∈ {𝑋} ∧ 𝑌 ∈ 𝐴)))) |
24 | 15, 23 | bitrd 268 |
. . 3
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴) → (𝑌◡(2nd ↾ ({𝑋} × 𝐴))〈𝑋, 𝑌〉 ↔ (𝑌 = 𝑌 ∧ (𝑋 ∈ {𝑋} ∧ 𝑌 ∈ 𝐴)))) |
25 | 11, 24 | bitrd 268 |
. 2
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴) → ((◡(2nd ↾ ({𝑋} × 𝐴))‘𝑌) = 〈𝑋, 𝑌〉 ↔ (𝑌 = 𝑌 ∧ (𝑋 ∈ {𝑋} ∧ 𝑌 ∈ 𝐴)))) |
26 | 4, 25 | mpbird 247 |
1
⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴) → (◡(2nd ↾ ({𝑋} × 𝐴))‘𝑌) = 〈𝑋, 𝑌〉) |