Proof of Theorem fv1stcnv
Step | Hyp | Ref
| Expression |
1 | | snidg 4550 |
. . . . 5
⊢ (𝑌 ∈ 𝑉 → 𝑌 ∈ {𝑌}) |
2 | 1 | anim2i 620 |
. . . 4
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑉) → (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ {𝑌})) |
3 | | eqid 2738 |
. . . 4
⊢ 𝑋 = 𝑋 |
4 | 2, 3 | jctir 524 |
. . 3
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑉) → ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ {𝑌}) ∧ 𝑋 = 𝑋)) |
5 | | opex 5322 |
. . . . . . 7
⊢
〈𝑋, 𝑌〉 ∈ V |
6 | | brcnvg 5722 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝐴 ∧ 〈𝑋, 𝑌〉 ∈ V) → (𝑋◡(1st ↾ (𝐴 × {𝑌}))〈𝑋, 𝑌〉 ↔ 〈𝑋, 𝑌〉(1st ↾ (𝐴 × {𝑌}))𝑋)) |
7 | 5, 6 | mpan2 691 |
. . . . . 6
⊢ (𝑋 ∈ 𝐴 → (𝑋◡(1st ↾ (𝐴 × {𝑌}))〈𝑋, 𝑌〉 ↔ 〈𝑋, 𝑌〉(1st ↾ (𝐴 × {𝑌}))𝑋)) |
8 | | brres 5832 |
. . . . . 6
⊢ (𝑋 ∈ 𝐴 → (〈𝑋, 𝑌〉(1st ↾ (𝐴 × {𝑌}))𝑋 ↔ (〈𝑋, 𝑌〉 ∈ (𝐴 × {𝑌}) ∧ 〈𝑋, 𝑌〉1st 𝑋))) |
9 | 7, 8 | bitrd 282 |
. . . . 5
⊢ (𝑋 ∈ 𝐴 → (𝑋◡(1st ↾ (𝐴 × {𝑌}))〈𝑋, 𝑌〉 ↔ (〈𝑋, 𝑌〉 ∈ (𝐴 × {𝑌}) ∧ 〈𝑋, 𝑌〉1st 𝑋))) |
10 | 9 | adantr 484 |
. . . 4
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑉) → (𝑋◡(1st ↾ (𝐴 × {𝑌}))〈𝑋, 𝑌〉 ↔ (〈𝑋, 𝑌〉 ∈ (𝐴 × {𝑌}) ∧ 〈𝑋, 𝑌〉1st 𝑋))) |
11 | | opelxp 5561 |
. . . . . 6
⊢
(〈𝑋, 𝑌〉 ∈ (𝐴 × {𝑌}) ↔ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ {𝑌})) |
12 | 11 | anbi1i 627 |
. . . . 5
⊢
((〈𝑋, 𝑌〉 ∈ (𝐴 × {𝑌}) ∧ 〈𝑋, 𝑌〉1st 𝑋) ↔ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ {𝑌}) ∧ 〈𝑋, 𝑌〉1st 𝑋)) |
13 | | br1steqg 7736 |
. . . . . 6
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑉) → (〈𝑋, 𝑌〉1st 𝑋 ↔ 𝑋 = 𝑋)) |
14 | 13 | anbi2d 632 |
. . . . 5
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑉) → (((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ {𝑌}) ∧ 〈𝑋, 𝑌〉1st 𝑋) ↔ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ {𝑌}) ∧ 𝑋 = 𝑋))) |
15 | 12, 14 | syl5bb 286 |
. . . 4
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑉) → ((〈𝑋, 𝑌〉 ∈ (𝐴 × {𝑌}) ∧ 〈𝑋, 𝑌〉1st 𝑋) ↔ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ {𝑌}) ∧ 𝑋 = 𝑋))) |
16 | 10, 15 | bitrd 282 |
. . 3
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑉) → (𝑋◡(1st ↾ (𝐴 × {𝑌}))〈𝑋, 𝑌〉 ↔ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ {𝑌}) ∧ 𝑋 = 𝑋))) |
17 | 4, 16 | mpbird 260 |
. 2
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑉) → 𝑋◡(1st ↾ (𝐴 × {𝑌}))〈𝑋, 𝑌〉) |
18 | | 1stconst 7821 |
. . . 4
⊢ (𝑌 ∈ 𝑉 → (1st ↾ (𝐴 × {𝑌})):(𝐴 × {𝑌})–1-1-onto→𝐴) |
19 | | f1ocnv 6630 |
. . . 4
⊢
((1st ↾ (𝐴 × {𝑌})):(𝐴 × {𝑌})–1-1-onto→𝐴 → ◡(1st ↾ (𝐴 × {𝑌})):𝐴–1-1-onto→(𝐴 × {𝑌})) |
20 | | f1ofn 6619 |
. . . 4
⊢ (◡(1st ↾ (𝐴 × {𝑌})):𝐴–1-1-onto→(𝐴 × {𝑌}) → ◡(1st ↾ (𝐴 × {𝑌})) Fn 𝐴) |
21 | 18, 19, 20 | 3syl 18 |
. . 3
⊢ (𝑌 ∈ 𝑉 → ◡(1st ↾ (𝐴 × {𝑌})) Fn 𝐴) |
22 | | simpl 486 |
. . 3
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑉) → 𝑋 ∈ 𝐴) |
23 | | fnbrfvb 6722 |
. . 3
⊢ ((◡(1st ↾ (𝐴 × {𝑌})) Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → ((◡(1st ↾ (𝐴 × {𝑌}))‘𝑋) = 〈𝑋, 𝑌〉 ↔ 𝑋◡(1st ↾ (𝐴 × {𝑌}))〈𝑋, 𝑌〉)) |
24 | 21, 22, 23 | syl2an2 686 |
. 2
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑉) → ((◡(1st ↾ (𝐴 × {𝑌}))‘𝑋) = 〈𝑋, 𝑌〉 ↔ 𝑋◡(1st ↾ (𝐴 × {𝑌}))〈𝑋, 𝑌〉)) |
25 | 17, 24 | mpbird 260 |
1
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑉) → (◡(1st ↾ (𝐴 × {𝑌}))‘𝑋) = 〈𝑋, 𝑌〉) |