Step | Hyp | Ref
| Expression |
1 | | snidg 4625 |
. . . . 5
⊢ (𝑌 ∈ 𝑉 → 𝑌 ∈ {𝑌}) |
2 | 1 | anim2i 618 |
. . . 4
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑉) → (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ {𝑌})) |
3 | | eqid 2737 |
. . . 4
⊢ 𝑋 = 𝑋 |
4 | 2, 3 | jctir 522 |
. . 3
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑉) → ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ {𝑌}) ∧ 𝑋 = 𝑋)) |
5 | | opex 5426 |
. . . . . . 7
⊢
⟨𝑋, 𝑌⟩ ∈ V |
6 | | brcnvg 5840 |
. . . . . . 7
⊢ ((𝑋 ∈ 𝐴 ∧ ⟨𝑋, 𝑌⟩ ∈ V) → (𝑋◡(1st ↾ (𝐴 × {𝑌}))⟨𝑋, 𝑌⟩ ↔ ⟨𝑋, 𝑌⟩(1st ↾ (𝐴 × {𝑌}))𝑋)) |
7 | 5, 6 | mpan2 690 |
. . . . . 6
⊢ (𝑋 ∈ 𝐴 → (𝑋◡(1st ↾ (𝐴 × {𝑌}))⟨𝑋, 𝑌⟩ ↔ ⟨𝑋, 𝑌⟩(1st ↾ (𝐴 × {𝑌}))𝑋)) |
8 | | brres 5949 |
. . . . . 6
⊢ (𝑋 ∈ 𝐴 → (⟨𝑋, 𝑌⟩(1st ↾ (𝐴 × {𝑌}))𝑋 ↔ (⟨𝑋, 𝑌⟩ ∈ (𝐴 × {𝑌}) ∧ ⟨𝑋, 𝑌⟩1st 𝑋))) |
9 | 7, 8 | bitrd 279 |
. . . . 5
⊢ (𝑋 ∈ 𝐴 → (𝑋◡(1st ↾ (𝐴 × {𝑌}))⟨𝑋, 𝑌⟩ ↔ (⟨𝑋, 𝑌⟩ ∈ (𝐴 × {𝑌}) ∧ ⟨𝑋, 𝑌⟩1st 𝑋))) |
10 | 9 | adantr 482 |
. . . 4
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑉) → (𝑋◡(1st ↾ (𝐴 × {𝑌}))⟨𝑋, 𝑌⟩ ↔ (⟨𝑋, 𝑌⟩ ∈ (𝐴 × {𝑌}) ∧ ⟨𝑋, 𝑌⟩1st 𝑋))) |
11 | | opelxp 5674 |
. . . . . 6
⊢
(⟨𝑋, 𝑌⟩ ∈ (𝐴 × {𝑌}) ↔ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ {𝑌})) |
12 | 11 | anbi1i 625 |
. . . . 5
⊢
((⟨𝑋, 𝑌⟩ ∈ (𝐴 × {𝑌}) ∧ ⟨𝑋, 𝑌⟩1st 𝑋) ↔ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ {𝑌}) ∧ ⟨𝑋, 𝑌⟩1st 𝑋)) |
13 | | br1steqg 7948 |
. . . . . 6
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑉) → (⟨𝑋, 𝑌⟩1st 𝑋 ↔ 𝑋 = 𝑋)) |
14 | 13 | anbi2d 630 |
. . . . 5
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑉) → (((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ {𝑌}) ∧ ⟨𝑋, 𝑌⟩1st 𝑋) ↔ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ {𝑌}) ∧ 𝑋 = 𝑋))) |
15 | 12, 14 | bitrid 283 |
. . . 4
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑉) → ((⟨𝑋, 𝑌⟩ ∈ (𝐴 × {𝑌}) ∧ ⟨𝑋, 𝑌⟩1st 𝑋) ↔ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ {𝑌}) ∧ 𝑋 = 𝑋))) |
16 | 10, 15 | bitrd 279 |
. . 3
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑉) → (𝑋◡(1st ↾ (𝐴 × {𝑌}))⟨𝑋, 𝑌⟩ ↔ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ {𝑌}) ∧ 𝑋 = 𝑋))) |
17 | 4, 16 | mpbird 257 |
. 2
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑉) → 𝑋◡(1st ↾ (𝐴 × {𝑌}))⟨𝑋, 𝑌⟩) |
18 | | 1stconst 8037 |
. . . 4
⊢ (𝑌 ∈ 𝑉 → (1st ↾ (𝐴 × {𝑌})):(𝐴 × {𝑌})–1-1-onto→𝐴) |
19 | | f1ocnv 6801 |
. . . 4
⊢
((1st ↾ (𝐴 × {𝑌})):(𝐴 × {𝑌})–1-1-onto→𝐴 → ◡(1st ↾ (𝐴 × {𝑌})):𝐴–1-1-onto→(𝐴 × {𝑌})) |
20 | | f1ofn 6790 |
. . . 4
⊢ (◡(1st ↾ (𝐴 × {𝑌})):𝐴–1-1-onto→(𝐴 × {𝑌}) → ◡(1st ↾ (𝐴 × {𝑌})) Fn 𝐴) |
21 | 18, 19, 20 | 3syl 18 |
. . 3
⊢ (𝑌 ∈ 𝑉 → ◡(1st ↾ (𝐴 × {𝑌})) Fn 𝐴) |
22 | | simpl 484 |
. . 3
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑉) → 𝑋 ∈ 𝐴) |
23 | | fnbrfvb 6900 |
. . 3
⊢ ((◡(1st ↾ (𝐴 × {𝑌})) Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → ((◡(1st ↾ (𝐴 × {𝑌}))‘𝑋) = ⟨𝑋, 𝑌⟩ ↔ 𝑋◡(1st ↾ (𝐴 × {𝑌}))⟨𝑋, 𝑌⟩)) |
24 | 21, 22, 23 | syl2an2 685 |
. 2
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑉) → ((◡(1st ↾ (𝐴 × {𝑌}))‘𝑋) = ⟨𝑋, 𝑌⟩ ↔ 𝑋◡(1st ↾ (𝐴 × {𝑌}))⟨𝑋, 𝑌⟩)) |
25 | 17, 24 | mpbird 257 |
1
⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝑉) → (◡(1st ↾ (𝐴 × {𝑌}))‘𝑋) = ⟨𝑋, 𝑌⟩) |