Proof of Theorem fv1stcnv
Step | Hyp | Ref
| Expression |
1 | | snidg 4153 |
. . . . 5
⊢ (𝑌 ∈ 𝑉 → 𝑌 ∈ {𝑌}) |
2 | 1 | anim2i 591 |
. . . 4
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑉) → (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ {𝑌})) |
3 | | eqid 2610 |
. . . 4
⊢ 𝑋 = 𝑋 |
4 | 2, 3 | jctil 558 |
. . 3
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑉) → (𝑋 = 𝑋 ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ {𝑌}))) |
5 | | opex 4859 |
. . . . . . 7
⊢
〈𝑋, 𝑌〉 ∈ V |
6 | | brcnvg 5225 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝐴 ∧ 〈𝑋, 𝑌〉 ∈ V) → (𝑋◡(1st ↾ (𝐴 × {𝑌}))〈𝑋, 𝑌〉 ↔ 〈𝑋, 𝑌〉(1st ↾ (𝐴 × {𝑌}))𝑋)) |
7 | 5, 6 | mpan2 703 |
. . . . . 6
⊢ (𝑋 ∈ 𝐴 → (𝑋◡(1st ↾ (𝐴 × {𝑌}))〈𝑋, 𝑌〉 ↔ 〈𝑋, 𝑌〉(1st ↾ (𝐴 × {𝑌}))𝑋)) |
8 | | brresg 5325 |
. . . . . 6
⊢ (𝑋 ∈ 𝐴 → (〈𝑋, 𝑌〉(1st ↾ (𝐴 × {𝑌}))𝑋 ↔ (〈𝑋, 𝑌〉1st 𝑋 ∧ 〈𝑋, 𝑌〉 ∈ (𝐴 × {𝑌})))) |
9 | 7, 8 | bitrd 267 |
. . . . 5
⊢ (𝑋 ∈ 𝐴 → (𝑋◡(1st ↾ (𝐴 × {𝑌}))〈𝑋, 𝑌〉 ↔ (〈𝑋, 𝑌〉1st 𝑋 ∧ 〈𝑋, 𝑌〉 ∈ (𝐴 × {𝑌})))) |
10 | 9 | adantr 480 |
. . . 4
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑉) → (𝑋◡(1st ↾ (𝐴 × {𝑌}))〈𝑋, 𝑌〉 ↔ (〈𝑋, 𝑌〉1st 𝑋 ∧ 〈𝑋, 𝑌〉 ∈ (𝐴 × {𝑌})))) |
11 | | opelxp 5070 |
. . . . . 6
⊢
(〈𝑋, 𝑌〉 ∈ (𝐴 × {𝑌}) ↔ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ {𝑌})) |
12 | 11 | anbi2i 726 |
. . . . 5
⊢
((〈𝑋, 𝑌〉1st 𝑋 ∧ 〈𝑋, 𝑌〉 ∈ (𝐴 × {𝑌})) ↔ (〈𝑋, 𝑌〉1st 𝑋 ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ {𝑌}))) |
13 | | br1steqg 30919 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ 𝐴) → (〈𝑋, 𝑌〉1st 𝑋 ↔ 𝑋 = 𝑋)) |
14 | 13 | 3anidm13 1376 |
. . . . . 6
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑉) → (〈𝑋, 𝑌〉1st 𝑋 ↔ 𝑋 = 𝑋)) |
15 | 14 | anbi1d 737 |
. . . . 5
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑉) → ((〈𝑋, 𝑌〉1st 𝑋 ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ {𝑌})) ↔ (𝑋 = 𝑋 ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ {𝑌})))) |
16 | 12, 15 | syl5bb 271 |
. . . 4
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑉) → ((〈𝑋, 𝑌〉1st 𝑋 ∧ 〈𝑋, 𝑌〉 ∈ (𝐴 × {𝑌})) ↔ (𝑋 = 𝑋 ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ {𝑌})))) |
17 | 10, 16 | bitrd 267 |
. . 3
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑉) → (𝑋◡(1st ↾ (𝐴 × {𝑌}))〈𝑋, 𝑌〉 ↔ (𝑋 = 𝑋 ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ {𝑌})))) |
18 | 4, 17 | mpbird 246 |
. 2
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑉) → 𝑋◡(1st ↾ (𝐴 × {𝑌}))〈𝑋, 𝑌〉) |
19 | | 1stconst 7152 |
. . . . 5
⊢ (𝑌 ∈ 𝑉 → (1st ↾ (𝐴 × {𝑌})):(𝐴 × {𝑌})–1-1-onto→𝐴) |
20 | | f1ocnv 6062 |
. . . . 5
⊢
((1st ↾ (𝐴 × {𝑌})):(𝐴 × {𝑌})–1-1-onto→𝐴 → ◡(1st ↾ (𝐴 × {𝑌})):𝐴–1-1-onto→(𝐴 × {𝑌})) |
21 | | f1ofn 6051 |
. . . . 5
⊢ (◡(1st ↾ (𝐴 × {𝑌})):𝐴–1-1-onto→(𝐴 × {𝑌}) → ◡(1st ↾ (𝐴 × {𝑌})) Fn 𝐴) |
22 | 19, 20, 21 | 3syl 18 |
. . . 4
⊢ (𝑌 ∈ 𝑉 → ◡(1st ↾ (𝐴 × {𝑌})) Fn 𝐴) |
23 | 22 | adantl 481 |
. . 3
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑉) → ◡(1st ↾ (𝐴 × {𝑌})) Fn 𝐴) |
24 | | simpl 472 |
. . 3
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑉) → 𝑋 ∈ 𝐴) |
25 | | fnbrfvb 6146 |
. . 3
⊢ ((◡(1st ↾ (𝐴 × {𝑌})) Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → ((◡(1st ↾ (𝐴 × {𝑌}))‘𝑋) = 〈𝑋, 𝑌〉 ↔ 𝑋◡(1st ↾ (𝐴 × {𝑌}))〈𝑋, 𝑌〉)) |
26 | 23, 24, 25 | syl2anc 691 |
. 2
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑉) → ((◡(1st ↾ (𝐴 × {𝑌}))‘𝑋) = 〈𝑋, 𝑌〉 ↔ 𝑋◡(1st ↾ (𝐴 × {𝑌}))〈𝑋, 𝑌〉)) |
27 | 18, 26 | mpbird 246 |
1
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑉) → (◡(1st ↾ (𝐴 × {𝑌}))‘𝑋) = 〈𝑋, 𝑌〉) |