Step | Hyp | Ref
| Expression |
1 | | df-ima 5051 |
. . 3
⊢ ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) “ (𝐴 × 𝐴)) = ran ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) ↾ (𝐴 × 𝐴)) |
2 | | simpr 476 |
. . . . 5
⊢ ((𝐹 Fn 𝑋 ∧ 𝐴 ⊆ 𝑋) → 𝐴 ⊆ 𝑋) |
3 | | resmpt2 6656 |
. . . . 5
⊢ ((𝐴 ⊆ 𝑋 ∧ 𝐴 ⊆ 𝑋) → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) ↾ (𝐴 × 𝐴)) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉)) |
4 | 2, 3 | sylancom 698 |
. . . 4
⊢ ((𝐹 Fn 𝑋 ∧ 𝐴 ⊆ 𝑋) → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) ↾ (𝐴 × 𝐴)) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉)) |
5 | 4 | rneqd 5274 |
. . 3
⊢ ((𝐹 Fn 𝑋 ∧ 𝐴 ⊆ 𝑋) → ran ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) ↾ (𝐴 × 𝐴)) = ran (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉)) |
6 | 1, 5 | syl5eq 2656 |
. 2
⊢ ((𝐹 Fn 𝑋 ∧ 𝐴 ⊆ 𝑋) → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) “ (𝐴 × 𝐴)) = ran (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉)) |
7 | | vex 3176 |
. . . . . . . . . . . . 13
⊢ 𝑥 ∈ V |
8 | | vex 3176 |
. . . . . . . . . . . . 13
⊢ 𝑦 ∈ V |
9 | 7, 8 | op1std 7069 |
. . . . . . . . . . . 12
⊢ (𝑝 = 〈𝑥, 𝑦〉 → (1st ‘𝑝) = 𝑥) |
10 | 9 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ (𝑝 = 〈𝑥, 𝑦〉 → (𝐹‘(1st ‘𝑝)) = (𝐹‘𝑥)) |
11 | 7, 8 | op2ndd 7070 |
. . . . . . . . . . . 12
⊢ (𝑝 = 〈𝑥, 𝑦〉 → (2nd ‘𝑝) = 𝑦) |
12 | 11 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ (𝑝 = 〈𝑥, 𝑦〉 → (𝐹‘(2nd ‘𝑝)) = (𝐹‘𝑦)) |
13 | 10, 12 | opeq12d 4348 |
. . . . . . . . . 10
⊢ (𝑝 = 〈𝑥, 𝑦〉 → 〈(𝐹‘(1st ‘𝑝)), (𝐹‘(2nd ‘𝑝))〉 = 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) |
14 | 13 | mpt2mpt 6650 |
. . . . . . . . 9
⊢ (𝑝 ∈ (𝐴 × 𝐴) ↦ 〈(𝐹‘(1st ‘𝑝)), (𝐹‘(2nd ‘𝑝))〉) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) |
15 | 14 | eqcomi 2619 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) = (𝑝 ∈ (𝐴 × 𝐴) ↦ 〈(𝐹‘(1st ‘𝑝)), (𝐹‘(2nd ‘𝑝))〉) |
16 | 15 | rneqi 5273 |
. . . . . . 7
⊢ ran
(𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) = ran (𝑝 ∈ (𝐴 × 𝐴) ↦ 〈(𝐹‘(1st ‘𝑝)), (𝐹‘(2nd ‘𝑝))〉) |
17 | | fvex 6113 |
. . . . . . . 8
⊢ (𝐹‘(1st
‘𝑝)) ∈
V |
18 | 17 | a1i 11 |
. . . . . . 7
⊢
((⊤ ∧ 𝑝
∈ (𝐴 × 𝐴)) → (𝐹‘(1st ‘𝑝)) ∈ V) |
19 | | fvex 6113 |
. . . . . . . 8
⊢ (𝐹‘(2nd
‘𝑝)) ∈
V |
20 | 19 | a1i 11 |
. . . . . . 7
⊢
((⊤ ∧ 𝑝
∈ (𝐴 × 𝐴)) → (𝐹‘(2nd ‘𝑝)) ∈ V) |
21 | 16, 18, 20 | fliftrel 6458 |
. . . . . 6
⊢ (⊤
→ ran (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) ⊆ (V ×
V)) |
22 | 21 | trud 1484 |
. . . . 5
⊢ ran
(𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) ⊆ (V ×
V) |
23 | 22 | sseli 3564 |
. . . 4
⊢ (𝑝 ∈ ran (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) → 𝑝 ∈ (V × V)) |
24 | 23 | adantl 481 |
. . 3
⊢ (((𝐹 Fn 𝑋 ∧ 𝐴 ⊆ 𝑋) ∧ 𝑝 ∈ ran (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉)) → 𝑝 ∈ (V × V)) |
25 | | xpss 5149 |
. . . . 5
⊢ ((𝐹 “ 𝐴) × (𝐹 “ 𝐴)) ⊆ (V × V) |
26 | 25 | sseli 3564 |
. . . 4
⊢ (𝑝 ∈ ((𝐹 “ 𝐴) × (𝐹 “ 𝐴)) → 𝑝 ∈ (V × V)) |
27 | 26 | adantl 481 |
. . 3
⊢ (((𝐹 Fn 𝑋 ∧ 𝐴 ⊆ 𝑋) ∧ 𝑝 ∈ ((𝐹 “ 𝐴) × (𝐹 “ 𝐴))) → 𝑝 ∈ (V × V)) |
28 | | fvelimab 6163 |
. . . . . . . 8
⊢ ((𝐹 Fn 𝑋 ∧ 𝐴 ⊆ 𝑋) → ((1st ‘𝑝) ∈ (𝐹 “ 𝐴) ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = (1st ‘𝑝))) |
29 | | fvelimab 6163 |
. . . . . . . 8
⊢ ((𝐹 Fn 𝑋 ∧ 𝐴 ⊆ 𝑋) → ((2nd ‘𝑝) ∈ (𝐹 “ 𝐴) ↔ ∃𝑦 ∈ 𝐴 (𝐹‘𝑦) = (2nd ‘𝑝))) |
30 | 28, 29 | anbi12d 743 |
. . . . . . 7
⊢ ((𝐹 Fn 𝑋 ∧ 𝐴 ⊆ 𝑋) → (((1st ‘𝑝) ∈ (𝐹 “ 𝐴) ∧ (2nd ‘𝑝) ∈ (𝐹 “ 𝐴)) ↔ (∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = (1st ‘𝑝) ∧ ∃𝑦 ∈ 𝐴 (𝐹‘𝑦) = (2nd ‘𝑝)))) |
31 | | eqid 2610 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) |
32 | | opex 4859 |
. . . . . . . . 9
⊢
〈(𝐹‘𝑥), (𝐹‘𝑦)〉 ∈ V |
33 | 31, 32 | elrnmpt2 6671 |
. . . . . . . 8
⊢
(〈(1st ‘𝑝), (2nd ‘𝑝)〉 ∈ ran (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 〈(1st ‘𝑝), (2nd ‘𝑝)〉 = 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) |
34 | | eqcom 2617 |
. . . . . . . . . 10
⊢
(〈(1st ‘𝑝), (2nd ‘𝑝)〉 = 〈(𝐹‘𝑥), (𝐹‘𝑦)〉 ↔ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉 = 〈(1st ‘𝑝), (2nd ‘𝑝)〉) |
35 | | fvex 6113 |
. . . . . . . . . . 11
⊢
(1st ‘𝑝) ∈ V |
36 | | fvex 6113 |
. . . . . . . . . . 11
⊢
(2nd ‘𝑝) ∈ V |
37 | 35, 36 | opth2 4875 |
. . . . . . . . . 10
⊢
(〈(𝐹‘𝑥), (𝐹‘𝑦)〉 = 〈(1st ‘𝑝), (2nd ‘𝑝)〉 ↔ ((𝐹‘𝑥) = (1st ‘𝑝) ∧ (𝐹‘𝑦) = (2nd ‘𝑝))) |
38 | 34, 37 | bitri 263 |
. . . . . . . . 9
⊢
(〈(1st ‘𝑝), (2nd ‘𝑝)〉 = 〈(𝐹‘𝑥), (𝐹‘𝑦)〉 ↔ ((𝐹‘𝑥) = (1st ‘𝑝) ∧ (𝐹‘𝑦) = (2nd ‘𝑝))) |
39 | 38 | 2rexbii 3024 |
. . . . . . . 8
⊢
(∃𝑥 ∈
𝐴 ∃𝑦 ∈ 𝐴 〈(1st ‘𝑝), (2nd ‘𝑝)〉 = 〈(𝐹‘𝑥), (𝐹‘𝑦)〉 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ((𝐹‘𝑥) = (1st ‘𝑝) ∧ (𝐹‘𝑦) = (2nd ‘𝑝))) |
40 | | reeanv 3086 |
. . . . . . . 8
⊢
(∃𝑥 ∈
𝐴 ∃𝑦 ∈ 𝐴 ((𝐹‘𝑥) = (1st ‘𝑝) ∧ (𝐹‘𝑦) = (2nd ‘𝑝)) ↔ (∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = (1st ‘𝑝) ∧ ∃𝑦 ∈ 𝐴 (𝐹‘𝑦) = (2nd ‘𝑝))) |
41 | 33, 39, 40 | 3bitri 285 |
. . . . . . 7
⊢
(〈(1st ‘𝑝), (2nd ‘𝑝)〉 ∈ ran (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) ↔ (∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = (1st ‘𝑝) ∧ ∃𝑦 ∈ 𝐴 (𝐹‘𝑦) = (2nd ‘𝑝))) |
42 | 30, 41 | syl6rbbr 278 |
. . . . . 6
⊢ ((𝐹 Fn 𝑋 ∧ 𝐴 ⊆ 𝑋) → (〈(1st ‘𝑝), (2nd ‘𝑝)〉 ∈ ran (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) ↔ ((1st ‘𝑝) ∈ (𝐹 “ 𝐴) ∧ (2nd ‘𝑝) ∈ (𝐹 “ 𝐴)))) |
43 | | opelxp 5070 |
. . . . . 6
⊢
(〈(1st ‘𝑝), (2nd ‘𝑝)〉 ∈ ((𝐹 “ 𝐴) × (𝐹 “ 𝐴)) ↔ ((1st ‘𝑝) ∈ (𝐹 “ 𝐴) ∧ (2nd ‘𝑝) ∈ (𝐹 “ 𝐴))) |
44 | 42, 43 | syl6bbr 277 |
. . . . 5
⊢ ((𝐹 Fn 𝑋 ∧ 𝐴 ⊆ 𝑋) → (〈(1st ‘𝑝), (2nd ‘𝑝)〉 ∈ ran (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) ↔ 〈(1st
‘𝑝), (2nd
‘𝑝)〉 ∈
((𝐹 “ 𝐴) × (𝐹 “ 𝐴)))) |
45 | 44 | adantr 480 |
. . . 4
⊢ (((𝐹 Fn 𝑋 ∧ 𝐴 ⊆ 𝑋) ∧ 𝑝 ∈ (V × V)) →
(〈(1st ‘𝑝), (2nd ‘𝑝)〉 ∈ ran (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) ↔ 〈(1st
‘𝑝), (2nd
‘𝑝)〉 ∈
((𝐹 “ 𝐴) × (𝐹 “ 𝐴)))) |
46 | | 1st2nd2 7096 |
. . . . . 6
⊢ (𝑝 ∈ (V × V) →
𝑝 = 〈(1st
‘𝑝), (2nd
‘𝑝)〉) |
47 | 46 | adantl 481 |
. . . . 5
⊢ (((𝐹 Fn 𝑋 ∧ 𝐴 ⊆ 𝑋) ∧ 𝑝 ∈ (V × V)) → 𝑝 = 〈(1st
‘𝑝), (2nd
‘𝑝)〉) |
48 | 47 | eleq1d 2672 |
. . . 4
⊢ (((𝐹 Fn 𝑋 ∧ 𝐴 ⊆ 𝑋) ∧ 𝑝 ∈ (V × V)) → (𝑝 ∈ ran (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) ↔ 〈(1st
‘𝑝), (2nd
‘𝑝)〉 ∈ ran
(𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉))) |
49 | 47 | eleq1d 2672 |
. . . 4
⊢ (((𝐹 Fn 𝑋 ∧ 𝐴 ⊆ 𝑋) ∧ 𝑝 ∈ (V × V)) → (𝑝 ∈ ((𝐹 “ 𝐴) × (𝐹 “ 𝐴)) ↔ 〈(1st ‘𝑝), (2nd ‘𝑝)〉 ∈ ((𝐹 “ 𝐴) × (𝐹 “ 𝐴)))) |
50 | 45, 48, 49 | 3bitr4d 299 |
. . 3
⊢ (((𝐹 Fn 𝑋 ∧ 𝐴 ⊆ 𝑋) ∧ 𝑝 ∈ (V × V)) → (𝑝 ∈ ran (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) ↔ 𝑝 ∈ ((𝐹 “ 𝐴) × (𝐹 “ 𝐴)))) |
51 | 24, 27, 50 | eqrdav 2609 |
. 2
⊢ ((𝐹 Fn 𝑋 ∧ 𝐴 ⊆ 𝑋) → ran (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) = ((𝐹 “ 𝐴) × (𝐹 “ 𝐴))) |
52 | 6, 51 | eqtrd 2644 |
1
⊢ ((𝐹 Fn 𝑋 ∧ 𝐴 ⊆ 𝑋) → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) “ (𝐴 × 𝐴)) = ((𝐹 “ 𝐴) × (𝐹 “ 𝐴))) |