Step | Hyp | Ref
| Expression |
1 | | df-ima 5368 |
. . 3
⊢ ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) “ (𝐴 × 𝐴)) = ran ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) ↾ (𝐴 × 𝐴)) |
2 | | simpr 479 |
. . . . 5
⊢ ((𝐹 Fn 𝑋 ∧ 𝐴 ⊆ 𝑋) → 𝐴 ⊆ 𝑋) |
3 | | resmpt2 7035 |
. . . . 5
⊢ ((𝐴 ⊆ 𝑋 ∧ 𝐴 ⊆ 𝑋) → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) ↾ (𝐴 × 𝐴)) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉)) |
4 | 2, 3 | sylancom 582 |
. . . 4
⊢ ((𝐹 Fn 𝑋 ∧ 𝐴 ⊆ 𝑋) → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) ↾ (𝐴 × 𝐴)) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉)) |
5 | 4 | rneqd 5598 |
. . 3
⊢ ((𝐹 Fn 𝑋 ∧ 𝐴 ⊆ 𝑋) → ran ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) ↾ (𝐴 × 𝐴)) = ran (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉)) |
6 | 1, 5 | syl5eq 2826 |
. 2
⊢ ((𝐹 Fn 𝑋 ∧ 𝐴 ⊆ 𝑋) → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) “ (𝐴 × 𝐴)) = ran (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉)) |
7 | | vex 3401 |
. . . . . . . . . . . . 13
⊢ 𝑥 ∈ V |
8 | | vex 3401 |
. . . . . . . . . . . . 13
⊢ 𝑦 ∈ V |
9 | 7, 8 | op1std 7455 |
. . . . . . . . . . . 12
⊢ (𝑝 = 〈𝑥, 𝑦〉 → (1st ‘𝑝) = 𝑥) |
10 | 9 | fveq2d 6450 |
. . . . . . . . . . 11
⊢ (𝑝 = 〈𝑥, 𝑦〉 → (𝐹‘(1st ‘𝑝)) = (𝐹‘𝑥)) |
11 | 7, 8 | op2ndd 7456 |
. . . . . . . . . . . 12
⊢ (𝑝 = 〈𝑥, 𝑦〉 → (2nd ‘𝑝) = 𝑦) |
12 | 11 | fveq2d 6450 |
. . . . . . . . . . 11
⊢ (𝑝 = 〈𝑥, 𝑦〉 → (𝐹‘(2nd ‘𝑝)) = (𝐹‘𝑦)) |
13 | 10, 12 | opeq12d 4644 |
. . . . . . . . . 10
⊢ (𝑝 = 〈𝑥, 𝑦〉 → 〈(𝐹‘(1st ‘𝑝)), (𝐹‘(2nd ‘𝑝))〉 = 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) |
14 | 13 | mpt2mpt 7029 |
. . . . . . . . 9
⊢ (𝑝 ∈ (𝐴 × 𝐴) ↦ 〈(𝐹‘(1st ‘𝑝)), (𝐹‘(2nd ‘𝑝))〉) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) |
15 | 14 | eqcomi 2787 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) = (𝑝 ∈ (𝐴 × 𝐴) ↦ 〈(𝐹‘(1st ‘𝑝)), (𝐹‘(2nd ‘𝑝))〉) |
16 | 15 | rneqi 5597 |
. . . . . . 7
⊢ ran
(𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) = ran (𝑝 ∈ (𝐴 × 𝐴) ↦ 〈(𝐹‘(1st ‘𝑝)), (𝐹‘(2nd ‘𝑝))〉) |
17 | | fvexd 6461 |
. . . . . . 7
⊢
((⊤ ∧ 𝑝
∈ (𝐴 × 𝐴)) → (𝐹‘(1st ‘𝑝)) ∈ V) |
18 | | fvexd 6461 |
. . . . . . 7
⊢
((⊤ ∧ 𝑝
∈ (𝐴 × 𝐴)) → (𝐹‘(2nd ‘𝑝)) ∈ V) |
19 | 16, 17, 18 | fliftrel 6830 |
. . . . . 6
⊢ (⊤
→ ran (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) ⊆ (V ×
V)) |
20 | 19 | mptru 1609 |
. . . . 5
⊢ ran
(𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) ⊆ (V ×
V) |
21 | 20 | sseli 3817 |
. . . 4
⊢ (𝑝 ∈ ran (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) → 𝑝 ∈ (V × V)) |
22 | 21 | adantl 475 |
. . 3
⊢ (((𝐹 Fn 𝑋 ∧ 𝐴 ⊆ 𝑋) ∧ 𝑝 ∈ ran (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉)) → 𝑝 ∈ (V × V)) |
23 | | xpss 5371 |
. . . . 5
⊢ ((𝐹 “ 𝐴) × (𝐹 “ 𝐴)) ⊆ (V × V) |
24 | 23 | sseli 3817 |
. . . 4
⊢ (𝑝 ∈ ((𝐹 “ 𝐴) × (𝐹 “ 𝐴)) → 𝑝 ∈ (V × V)) |
25 | 24 | adantl 475 |
. . 3
⊢ (((𝐹 Fn 𝑋 ∧ 𝐴 ⊆ 𝑋) ∧ 𝑝 ∈ ((𝐹 “ 𝐴) × (𝐹 “ 𝐴))) → 𝑝 ∈ (V × V)) |
26 | | fvelimab 6513 |
. . . . . . . 8
⊢ ((𝐹 Fn 𝑋 ∧ 𝐴 ⊆ 𝑋) → ((1st ‘𝑝) ∈ (𝐹 “ 𝐴) ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = (1st ‘𝑝))) |
27 | | fvelimab 6513 |
. . . . . . . 8
⊢ ((𝐹 Fn 𝑋 ∧ 𝐴 ⊆ 𝑋) → ((2nd ‘𝑝) ∈ (𝐹 “ 𝐴) ↔ ∃𝑦 ∈ 𝐴 (𝐹‘𝑦) = (2nd ‘𝑝))) |
28 | 26, 27 | anbi12d 624 |
. . . . . . 7
⊢ ((𝐹 Fn 𝑋 ∧ 𝐴 ⊆ 𝑋) → (((1st ‘𝑝) ∈ (𝐹 “ 𝐴) ∧ (2nd ‘𝑝) ∈ (𝐹 “ 𝐴)) ↔ (∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = (1st ‘𝑝) ∧ ∃𝑦 ∈ 𝐴 (𝐹‘𝑦) = (2nd ‘𝑝)))) |
29 | | eqid 2778 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) |
30 | | opex 5164 |
. . . . . . . . 9
⊢
〈(𝐹‘𝑥), (𝐹‘𝑦)〉 ∈ V |
31 | 29, 30 | elrnmpt2 7050 |
. . . . . . . 8
⊢
(〈(1st ‘𝑝), (2nd ‘𝑝)〉 ∈ ran (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 〈(1st ‘𝑝), (2nd ‘𝑝)〉 = 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) |
32 | | eqcom 2785 |
. . . . . . . . . 10
⊢
(〈(1st ‘𝑝), (2nd ‘𝑝)〉 = 〈(𝐹‘𝑥), (𝐹‘𝑦)〉 ↔ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉 = 〈(1st ‘𝑝), (2nd ‘𝑝)〉) |
33 | | fvex 6459 |
. . . . . . . . . . 11
⊢
(1st ‘𝑝) ∈ V |
34 | | fvex 6459 |
. . . . . . . . . . 11
⊢
(2nd ‘𝑝) ∈ V |
35 | 33, 34 | opth2 5180 |
. . . . . . . . . 10
⊢
(〈(𝐹‘𝑥), (𝐹‘𝑦)〉 = 〈(1st ‘𝑝), (2nd ‘𝑝)〉 ↔ ((𝐹‘𝑥) = (1st ‘𝑝) ∧ (𝐹‘𝑦) = (2nd ‘𝑝))) |
36 | 32, 35 | bitri 267 |
. . . . . . . . 9
⊢
(〈(1st ‘𝑝), (2nd ‘𝑝)〉 = 〈(𝐹‘𝑥), (𝐹‘𝑦)〉 ↔ ((𝐹‘𝑥) = (1st ‘𝑝) ∧ (𝐹‘𝑦) = (2nd ‘𝑝))) |
37 | 36 | 2rexbii 3225 |
. . . . . . . 8
⊢
(∃𝑥 ∈
𝐴 ∃𝑦 ∈ 𝐴 〈(1st ‘𝑝), (2nd ‘𝑝)〉 = 〈(𝐹‘𝑥), (𝐹‘𝑦)〉 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ((𝐹‘𝑥) = (1st ‘𝑝) ∧ (𝐹‘𝑦) = (2nd ‘𝑝))) |
38 | | reeanv 3293 |
. . . . . . . 8
⊢
(∃𝑥 ∈
𝐴 ∃𝑦 ∈ 𝐴 ((𝐹‘𝑥) = (1st ‘𝑝) ∧ (𝐹‘𝑦) = (2nd ‘𝑝)) ↔ (∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = (1st ‘𝑝) ∧ ∃𝑦 ∈ 𝐴 (𝐹‘𝑦) = (2nd ‘𝑝))) |
39 | 31, 37, 38 | 3bitri 289 |
. . . . . . 7
⊢
(〈(1st ‘𝑝), (2nd ‘𝑝)〉 ∈ ran (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) ↔ (∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = (1st ‘𝑝) ∧ ∃𝑦 ∈ 𝐴 (𝐹‘𝑦) = (2nd ‘𝑝))) |
40 | 28, 39 | syl6rbbr 282 |
. . . . . 6
⊢ ((𝐹 Fn 𝑋 ∧ 𝐴 ⊆ 𝑋) → (〈(1st ‘𝑝), (2nd ‘𝑝)〉 ∈ ran (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) ↔ ((1st ‘𝑝) ∈ (𝐹 “ 𝐴) ∧ (2nd ‘𝑝) ∈ (𝐹 “ 𝐴)))) |
41 | | opelxp 5391 |
. . . . . 6
⊢
(〈(1st ‘𝑝), (2nd ‘𝑝)〉 ∈ ((𝐹 “ 𝐴) × (𝐹 “ 𝐴)) ↔ ((1st ‘𝑝) ∈ (𝐹 “ 𝐴) ∧ (2nd ‘𝑝) ∈ (𝐹 “ 𝐴))) |
42 | 40, 41 | syl6bbr 281 |
. . . . 5
⊢ ((𝐹 Fn 𝑋 ∧ 𝐴 ⊆ 𝑋) → (〈(1st ‘𝑝), (2nd ‘𝑝)〉 ∈ ran (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) ↔ 〈(1st
‘𝑝), (2nd
‘𝑝)〉 ∈
((𝐹 “ 𝐴) × (𝐹 “ 𝐴)))) |
43 | 42 | adantr 474 |
. . . 4
⊢ (((𝐹 Fn 𝑋 ∧ 𝐴 ⊆ 𝑋) ∧ 𝑝 ∈ (V × V)) →
(〈(1st ‘𝑝), (2nd ‘𝑝)〉 ∈ ran (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) ↔ 〈(1st
‘𝑝), (2nd
‘𝑝)〉 ∈
((𝐹 “ 𝐴) × (𝐹 “ 𝐴)))) |
44 | | 1st2nd2 7484 |
. . . . . 6
⊢ (𝑝 ∈ (V × V) →
𝑝 = 〈(1st
‘𝑝), (2nd
‘𝑝)〉) |
45 | 44 | adantl 475 |
. . . . 5
⊢ (((𝐹 Fn 𝑋 ∧ 𝐴 ⊆ 𝑋) ∧ 𝑝 ∈ (V × V)) → 𝑝 = 〈(1st
‘𝑝), (2nd
‘𝑝)〉) |
46 | 45 | eleq1d 2844 |
. . . 4
⊢ (((𝐹 Fn 𝑋 ∧ 𝐴 ⊆ 𝑋) ∧ 𝑝 ∈ (V × V)) → (𝑝 ∈ ran (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) ↔ 〈(1st
‘𝑝), (2nd
‘𝑝)〉 ∈ ran
(𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉))) |
47 | 45 | eleq1d 2844 |
. . . 4
⊢ (((𝐹 Fn 𝑋 ∧ 𝐴 ⊆ 𝑋) ∧ 𝑝 ∈ (V × V)) → (𝑝 ∈ ((𝐹 “ 𝐴) × (𝐹 “ 𝐴)) ↔ 〈(1st ‘𝑝), (2nd ‘𝑝)〉 ∈ ((𝐹 “ 𝐴) × (𝐹 “ 𝐴)))) |
48 | 43, 46, 47 | 3bitr4d 303 |
. . 3
⊢ (((𝐹 Fn 𝑋 ∧ 𝐴 ⊆ 𝑋) ∧ 𝑝 ∈ (V × V)) → (𝑝 ∈ ran (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) ↔ 𝑝 ∈ ((𝐹 “ 𝐴) × (𝐹 “ 𝐴)))) |
49 | 22, 25, 48 | eqrdav 2777 |
. 2
⊢ ((𝐹 Fn 𝑋 ∧ 𝐴 ⊆ 𝑋) → ran (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) = ((𝐹 “ 𝐴) × (𝐹 “ 𝐴))) |
50 | 6, 49 | eqtrd 2814 |
1
⊢ ((𝐹 Fn 𝑋 ∧ 𝐴 ⊆ 𝑋) → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) “ (𝐴 × 𝐴)) = ((𝐹 “ 𝐴) × (𝐹 “ 𝐴))) |