Step | Hyp | Ref
| Expression |
1 | | df-ima 5570 |
. . 3
⊢ ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) “ (𝐴 × 𝐴)) = ran ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) ↾ (𝐴 × 𝐴)) |
2 | | simpr 487 |
. . . . 5
⊢ ((𝐹 Fn 𝑋 ∧ 𝐴 ⊆ 𝑋) → 𝐴 ⊆ 𝑋) |
3 | | resmpo 7274 |
. . . . 5
⊢ ((𝐴 ⊆ 𝑋 ∧ 𝐴 ⊆ 𝑋) → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) ↾ (𝐴 × 𝐴)) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉)) |
4 | 2, 3 | sylancom 590 |
. . . 4
⊢ ((𝐹 Fn 𝑋 ∧ 𝐴 ⊆ 𝑋) → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) ↾ (𝐴 × 𝐴)) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉)) |
5 | 4 | rneqd 5810 |
. . 3
⊢ ((𝐹 Fn 𝑋 ∧ 𝐴 ⊆ 𝑋) → ran ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) ↾ (𝐴 × 𝐴)) = ran (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉)) |
6 | 1, 5 | syl5eq 2870 |
. 2
⊢ ((𝐹 Fn 𝑋 ∧ 𝐴 ⊆ 𝑋) → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) “ (𝐴 × 𝐴)) = ran (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉)) |
7 | | vex 3499 |
. . . . . . . . . . . . 13
⊢ 𝑥 ∈ V |
8 | | vex 3499 |
. . . . . . . . . . . . 13
⊢ 𝑦 ∈ V |
9 | 7, 8 | op1std 7701 |
. . . . . . . . . . . 12
⊢ (𝑝 = 〈𝑥, 𝑦〉 → (1st ‘𝑝) = 𝑥) |
10 | 9 | fveq2d 6676 |
. . . . . . . . . . 11
⊢ (𝑝 = 〈𝑥, 𝑦〉 → (𝐹‘(1st ‘𝑝)) = (𝐹‘𝑥)) |
11 | 7, 8 | op2ndd 7702 |
. . . . . . . . . . . 12
⊢ (𝑝 = 〈𝑥, 𝑦〉 → (2nd ‘𝑝) = 𝑦) |
12 | 11 | fveq2d 6676 |
. . . . . . . . . . 11
⊢ (𝑝 = 〈𝑥, 𝑦〉 → (𝐹‘(2nd ‘𝑝)) = (𝐹‘𝑦)) |
13 | 10, 12 | opeq12d 4813 |
. . . . . . . . . 10
⊢ (𝑝 = 〈𝑥, 𝑦〉 → 〈(𝐹‘(1st ‘𝑝)), (𝐹‘(2nd ‘𝑝))〉 = 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) |
14 | 13 | mpompt 7268 |
. . . . . . . . 9
⊢ (𝑝 ∈ (𝐴 × 𝐴) ↦ 〈(𝐹‘(1st ‘𝑝)), (𝐹‘(2nd ‘𝑝))〉) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) |
15 | 14 | eqcomi 2832 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) = (𝑝 ∈ (𝐴 × 𝐴) ↦ 〈(𝐹‘(1st ‘𝑝)), (𝐹‘(2nd ‘𝑝))〉) |
16 | 15 | rneqi 5809 |
. . . . . . 7
⊢ ran
(𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) = ran (𝑝 ∈ (𝐴 × 𝐴) ↦ 〈(𝐹‘(1st ‘𝑝)), (𝐹‘(2nd ‘𝑝))〉) |
17 | | fvexd 6687 |
. . . . . . 7
⊢
((⊤ ∧ 𝑝
∈ (𝐴 × 𝐴)) → (𝐹‘(1st ‘𝑝)) ∈ V) |
18 | | fvexd 6687 |
. . . . . . 7
⊢
((⊤ ∧ 𝑝
∈ (𝐴 × 𝐴)) → (𝐹‘(2nd ‘𝑝)) ∈ V) |
19 | 16, 17, 18 | fliftrel 7063 |
. . . . . 6
⊢ (⊤
→ ran (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) ⊆ (V ×
V)) |
20 | 19 | mptru 1544 |
. . . . 5
⊢ ran
(𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) ⊆ (V ×
V) |
21 | 20 | sseli 3965 |
. . . 4
⊢ (𝑝 ∈ ran (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) → 𝑝 ∈ (V × V)) |
22 | 21 | adantl 484 |
. . 3
⊢ (((𝐹 Fn 𝑋 ∧ 𝐴 ⊆ 𝑋) ∧ 𝑝 ∈ ran (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉)) → 𝑝 ∈ (V × V)) |
23 | | xpss 5573 |
. . . . 5
⊢ ((𝐹 “ 𝐴) × (𝐹 “ 𝐴)) ⊆ (V × V) |
24 | 23 | sseli 3965 |
. . . 4
⊢ (𝑝 ∈ ((𝐹 “ 𝐴) × (𝐹 “ 𝐴)) → 𝑝 ∈ (V × V)) |
25 | 24 | adantl 484 |
. . 3
⊢ (((𝐹 Fn 𝑋 ∧ 𝐴 ⊆ 𝑋) ∧ 𝑝 ∈ ((𝐹 “ 𝐴) × (𝐹 “ 𝐴))) → 𝑝 ∈ (V × V)) |
26 | | fvelimab 6739 |
. . . . . . . 8
⊢ ((𝐹 Fn 𝑋 ∧ 𝐴 ⊆ 𝑋) → ((1st ‘𝑝) ∈ (𝐹 “ 𝐴) ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = (1st ‘𝑝))) |
27 | | fvelimab 6739 |
. . . . . . . 8
⊢ ((𝐹 Fn 𝑋 ∧ 𝐴 ⊆ 𝑋) → ((2nd ‘𝑝) ∈ (𝐹 “ 𝐴) ↔ ∃𝑦 ∈ 𝐴 (𝐹‘𝑦) = (2nd ‘𝑝))) |
28 | 26, 27 | anbi12d 632 |
. . . . . . 7
⊢ ((𝐹 Fn 𝑋 ∧ 𝐴 ⊆ 𝑋) → (((1st ‘𝑝) ∈ (𝐹 “ 𝐴) ∧ (2nd ‘𝑝) ∈ (𝐹 “ 𝐴)) ↔ (∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = (1st ‘𝑝) ∧ ∃𝑦 ∈ 𝐴 (𝐹‘𝑦) = (2nd ‘𝑝)))) |
29 | | eqid 2823 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) |
30 | | opex 5358 |
. . . . . . . . 9
⊢
〈(𝐹‘𝑥), (𝐹‘𝑦)〉 ∈ V |
31 | 29, 30 | elrnmpo 7289 |
. . . . . . . 8
⊢
(〈(1st ‘𝑝), (2nd ‘𝑝)〉 ∈ ran (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 〈(1st ‘𝑝), (2nd ‘𝑝)〉 = 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) |
32 | | eqcom 2830 |
. . . . . . . . . 10
⊢
(〈(1st ‘𝑝), (2nd ‘𝑝)〉 = 〈(𝐹‘𝑥), (𝐹‘𝑦)〉 ↔ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉 = 〈(1st ‘𝑝), (2nd ‘𝑝)〉) |
33 | | fvex 6685 |
. . . . . . . . . . 11
⊢
(1st ‘𝑝) ∈ V |
34 | | fvex 6685 |
. . . . . . . . . . 11
⊢
(2nd ‘𝑝) ∈ V |
35 | 33, 34 | opth2 5374 |
. . . . . . . . . 10
⊢
(〈(𝐹‘𝑥), (𝐹‘𝑦)〉 = 〈(1st ‘𝑝), (2nd ‘𝑝)〉 ↔ ((𝐹‘𝑥) = (1st ‘𝑝) ∧ (𝐹‘𝑦) = (2nd ‘𝑝))) |
36 | 32, 35 | bitri 277 |
. . . . . . . . 9
⊢
(〈(1st ‘𝑝), (2nd ‘𝑝)〉 = 〈(𝐹‘𝑥), (𝐹‘𝑦)〉 ↔ ((𝐹‘𝑥) = (1st ‘𝑝) ∧ (𝐹‘𝑦) = (2nd ‘𝑝))) |
37 | 36 | 2rexbii 3250 |
. . . . . . . 8
⊢
(∃𝑥 ∈
𝐴 ∃𝑦 ∈ 𝐴 〈(1st ‘𝑝), (2nd ‘𝑝)〉 = 〈(𝐹‘𝑥), (𝐹‘𝑦)〉 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ((𝐹‘𝑥) = (1st ‘𝑝) ∧ (𝐹‘𝑦) = (2nd ‘𝑝))) |
38 | | reeanv 3369 |
. . . . . . . 8
⊢
(∃𝑥 ∈
𝐴 ∃𝑦 ∈ 𝐴 ((𝐹‘𝑥) = (1st ‘𝑝) ∧ (𝐹‘𝑦) = (2nd ‘𝑝)) ↔ (∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = (1st ‘𝑝) ∧ ∃𝑦 ∈ 𝐴 (𝐹‘𝑦) = (2nd ‘𝑝))) |
39 | 31, 37, 38 | 3bitri 299 |
. . . . . . 7
⊢
(〈(1st ‘𝑝), (2nd ‘𝑝)〉 ∈ ran (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) ↔ (∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = (1st ‘𝑝) ∧ ∃𝑦 ∈ 𝐴 (𝐹‘𝑦) = (2nd ‘𝑝))) |
40 | 28, 39 | syl6rbbr 292 |
. . . . . 6
⊢ ((𝐹 Fn 𝑋 ∧ 𝐴 ⊆ 𝑋) → (〈(1st ‘𝑝), (2nd ‘𝑝)〉 ∈ ran (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) ↔ ((1st ‘𝑝) ∈ (𝐹 “ 𝐴) ∧ (2nd ‘𝑝) ∈ (𝐹 “ 𝐴)))) |
41 | | opelxp 5593 |
. . . . . 6
⊢
(〈(1st ‘𝑝), (2nd ‘𝑝)〉 ∈ ((𝐹 “ 𝐴) × (𝐹 “ 𝐴)) ↔ ((1st ‘𝑝) ∈ (𝐹 “ 𝐴) ∧ (2nd ‘𝑝) ∈ (𝐹 “ 𝐴))) |
42 | 40, 41 | syl6bbr 291 |
. . . . 5
⊢ ((𝐹 Fn 𝑋 ∧ 𝐴 ⊆ 𝑋) → (〈(1st ‘𝑝), (2nd ‘𝑝)〉 ∈ ran (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) ↔ 〈(1st
‘𝑝), (2nd
‘𝑝)〉 ∈
((𝐹 “ 𝐴) × (𝐹 “ 𝐴)))) |
43 | 42 | adantr 483 |
. . . 4
⊢ (((𝐹 Fn 𝑋 ∧ 𝐴 ⊆ 𝑋) ∧ 𝑝 ∈ (V × V)) →
(〈(1st ‘𝑝), (2nd ‘𝑝)〉 ∈ ran (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) ↔ 〈(1st
‘𝑝), (2nd
‘𝑝)〉 ∈
((𝐹 “ 𝐴) × (𝐹 “ 𝐴)))) |
44 | | 1st2nd2 7730 |
. . . . . 6
⊢ (𝑝 ∈ (V × V) →
𝑝 = 〈(1st
‘𝑝), (2nd
‘𝑝)〉) |
45 | 44 | adantl 484 |
. . . . 5
⊢ (((𝐹 Fn 𝑋 ∧ 𝐴 ⊆ 𝑋) ∧ 𝑝 ∈ (V × V)) → 𝑝 = 〈(1st
‘𝑝), (2nd
‘𝑝)〉) |
46 | 45 | eleq1d 2899 |
. . . 4
⊢ (((𝐹 Fn 𝑋 ∧ 𝐴 ⊆ 𝑋) ∧ 𝑝 ∈ (V × V)) → (𝑝 ∈ ran (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) ↔ 〈(1st
‘𝑝), (2nd
‘𝑝)〉 ∈ ran
(𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉))) |
47 | 45 | eleq1d 2899 |
. . . 4
⊢ (((𝐹 Fn 𝑋 ∧ 𝐴 ⊆ 𝑋) ∧ 𝑝 ∈ (V × V)) → (𝑝 ∈ ((𝐹 “ 𝐴) × (𝐹 “ 𝐴)) ↔ 〈(1st ‘𝑝), (2nd ‘𝑝)〉 ∈ ((𝐹 “ 𝐴) × (𝐹 “ 𝐴)))) |
48 | 43, 46, 47 | 3bitr4d 313 |
. . 3
⊢ (((𝐹 Fn 𝑋 ∧ 𝐴 ⊆ 𝑋) ∧ 𝑝 ∈ (V × V)) → (𝑝 ∈ ran (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) ↔ 𝑝 ∈ ((𝐹 “ 𝐴) × (𝐹 “ 𝐴)))) |
49 | 22, 25, 48 | eqrdav 2822 |
. 2
⊢ ((𝐹 Fn 𝑋 ∧ 𝐴 ⊆ 𝑋) → ran (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) = ((𝐹 “ 𝐴) × (𝐹 “ 𝐴))) |
50 | 6, 49 | eqtrd 2858 |
1
⊢ ((𝐹 Fn 𝑋 ∧ 𝐴 ⊆ 𝑋) → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) “ (𝐴 × 𝐴)) = ((𝐹 “ 𝐴) × (𝐹 “ 𝐴))) |