| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | df-ima 5698 | . . 3
⊢ ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) “ (𝐴 × 𝐴)) = ran ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) ↾ (𝐴 × 𝐴)) | 
| 2 |  | simpr 484 | . . . . 5
⊢ ((𝐹 Fn 𝑋 ∧ 𝐴 ⊆ 𝑋) → 𝐴 ⊆ 𝑋) | 
| 3 |  | resmpo 7553 | . . . . 5
⊢ ((𝐴 ⊆ 𝑋 ∧ 𝐴 ⊆ 𝑋) → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) ↾ (𝐴 × 𝐴)) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉)) | 
| 4 | 2, 3 | sylancom 588 | . . . 4
⊢ ((𝐹 Fn 𝑋 ∧ 𝐴 ⊆ 𝑋) → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) ↾ (𝐴 × 𝐴)) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉)) | 
| 5 | 4 | rneqd 5949 | . . 3
⊢ ((𝐹 Fn 𝑋 ∧ 𝐴 ⊆ 𝑋) → ran ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) ↾ (𝐴 × 𝐴)) = ran (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉)) | 
| 6 | 1, 5 | eqtrid 2789 | . 2
⊢ ((𝐹 Fn 𝑋 ∧ 𝐴 ⊆ 𝑋) → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) “ (𝐴 × 𝐴)) = ran (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉)) | 
| 7 |  | vex 3484 | . . . . . . . . . . . . 13
⊢ 𝑥 ∈ V | 
| 8 |  | vex 3484 | . . . . . . . . . . . . 13
⊢ 𝑦 ∈ V | 
| 9 | 7, 8 | op1std 8024 | . . . . . . . . . . . 12
⊢ (𝑝 = 〈𝑥, 𝑦〉 → (1st ‘𝑝) = 𝑥) | 
| 10 | 9 | fveq2d 6910 | . . . . . . . . . . 11
⊢ (𝑝 = 〈𝑥, 𝑦〉 → (𝐹‘(1st ‘𝑝)) = (𝐹‘𝑥)) | 
| 11 | 7, 8 | op2ndd 8025 | . . . . . . . . . . . 12
⊢ (𝑝 = 〈𝑥, 𝑦〉 → (2nd ‘𝑝) = 𝑦) | 
| 12 | 11 | fveq2d 6910 | . . . . . . . . . . 11
⊢ (𝑝 = 〈𝑥, 𝑦〉 → (𝐹‘(2nd ‘𝑝)) = (𝐹‘𝑦)) | 
| 13 | 10, 12 | opeq12d 4881 | . . . . . . . . . 10
⊢ (𝑝 = 〈𝑥, 𝑦〉 → 〈(𝐹‘(1st ‘𝑝)), (𝐹‘(2nd ‘𝑝))〉 = 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) | 
| 14 | 13 | mpompt 7547 | . . . . . . . . 9
⊢ (𝑝 ∈ (𝐴 × 𝐴) ↦ 〈(𝐹‘(1st ‘𝑝)), (𝐹‘(2nd ‘𝑝))〉) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) | 
| 15 | 14 | eqcomi 2746 | . . . . . . . 8
⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) = (𝑝 ∈ (𝐴 × 𝐴) ↦ 〈(𝐹‘(1st ‘𝑝)), (𝐹‘(2nd ‘𝑝))〉) | 
| 16 | 15 | rneqi 5948 | . . . . . . 7
⊢ ran
(𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) = ran (𝑝 ∈ (𝐴 × 𝐴) ↦ 〈(𝐹‘(1st ‘𝑝)), (𝐹‘(2nd ‘𝑝))〉) | 
| 17 |  | fvexd 6921 | . . . . . . 7
⊢
((⊤ ∧ 𝑝
∈ (𝐴 × 𝐴)) → (𝐹‘(1st ‘𝑝)) ∈ V) | 
| 18 |  | fvexd 6921 | . . . . . . 7
⊢
((⊤ ∧ 𝑝
∈ (𝐴 × 𝐴)) → (𝐹‘(2nd ‘𝑝)) ∈ V) | 
| 19 | 16, 17, 18 | fliftrel 7328 | . . . . . 6
⊢ (⊤
→ ran (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) ⊆ (V ×
V)) | 
| 20 | 19 | mptru 1547 | . . . . 5
⊢ ran
(𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) ⊆ (V ×
V) | 
| 21 | 20 | sseli 3979 | . . . 4
⊢ (𝑝 ∈ ran (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) → 𝑝 ∈ (V × V)) | 
| 22 | 21 | adantl 481 | . . 3
⊢ (((𝐹 Fn 𝑋 ∧ 𝐴 ⊆ 𝑋) ∧ 𝑝 ∈ ran (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉)) → 𝑝 ∈ (V × V)) | 
| 23 |  | xpss 5701 | . . . . 5
⊢ ((𝐹 “ 𝐴) × (𝐹 “ 𝐴)) ⊆ (V × V) | 
| 24 | 23 | sseli 3979 | . . . 4
⊢ (𝑝 ∈ ((𝐹 “ 𝐴) × (𝐹 “ 𝐴)) → 𝑝 ∈ (V × V)) | 
| 25 | 24 | adantl 481 | . . 3
⊢ (((𝐹 Fn 𝑋 ∧ 𝐴 ⊆ 𝑋) ∧ 𝑝 ∈ ((𝐹 “ 𝐴) × (𝐹 “ 𝐴))) → 𝑝 ∈ (V × V)) | 
| 26 |  | eqid 2737 | . . . . . . . . 9
⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) | 
| 27 |  | opex 5469 | . . . . . . . . 9
⊢
〈(𝐹‘𝑥), (𝐹‘𝑦)〉 ∈ V | 
| 28 | 26, 27 | elrnmpo 7569 | . . . . . . . 8
⊢
(〈(1st ‘𝑝), (2nd ‘𝑝)〉 ∈ ran (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 〈(1st ‘𝑝), (2nd ‘𝑝)〉 = 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) | 
| 29 |  | eqcom 2744 | . . . . . . . . . 10
⊢
(〈(1st ‘𝑝), (2nd ‘𝑝)〉 = 〈(𝐹‘𝑥), (𝐹‘𝑦)〉 ↔ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉 = 〈(1st ‘𝑝), (2nd ‘𝑝)〉) | 
| 30 |  | fvex 6919 | . . . . . . . . . . 11
⊢
(1st ‘𝑝) ∈ V | 
| 31 |  | fvex 6919 | . . . . . . . . . . 11
⊢
(2nd ‘𝑝) ∈ V | 
| 32 | 30, 31 | opth2 5485 | . . . . . . . . . 10
⊢
(〈(𝐹‘𝑥), (𝐹‘𝑦)〉 = 〈(1st ‘𝑝), (2nd ‘𝑝)〉 ↔ ((𝐹‘𝑥) = (1st ‘𝑝) ∧ (𝐹‘𝑦) = (2nd ‘𝑝))) | 
| 33 | 29, 32 | bitri 275 | . . . . . . . . 9
⊢
(〈(1st ‘𝑝), (2nd ‘𝑝)〉 = 〈(𝐹‘𝑥), (𝐹‘𝑦)〉 ↔ ((𝐹‘𝑥) = (1st ‘𝑝) ∧ (𝐹‘𝑦) = (2nd ‘𝑝))) | 
| 34 | 33 | 2rexbii 3129 | . . . . . . . 8
⊢
(∃𝑥 ∈
𝐴 ∃𝑦 ∈ 𝐴 〈(1st ‘𝑝), (2nd ‘𝑝)〉 = 〈(𝐹‘𝑥), (𝐹‘𝑦)〉 ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐴 ((𝐹‘𝑥) = (1st ‘𝑝) ∧ (𝐹‘𝑦) = (2nd ‘𝑝))) | 
| 35 |  | reeanv 3229 | . . . . . . . 8
⊢
(∃𝑥 ∈
𝐴 ∃𝑦 ∈ 𝐴 ((𝐹‘𝑥) = (1st ‘𝑝) ∧ (𝐹‘𝑦) = (2nd ‘𝑝)) ↔ (∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = (1st ‘𝑝) ∧ ∃𝑦 ∈ 𝐴 (𝐹‘𝑦) = (2nd ‘𝑝))) | 
| 36 | 28, 34, 35 | 3bitri 297 | . . . . . . 7
⊢
(〈(1st ‘𝑝), (2nd ‘𝑝)〉 ∈ ran (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) ↔ (∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = (1st ‘𝑝) ∧ ∃𝑦 ∈ 𝐴 (𝐹‘𝑦) = (2nd ‘𝑝))) | 
| 37 |  | fvelimab 6981 | . . . . . . . 8
⊢ ((𝐹 Fn 𝑋 ∧ 𝐴 ⊆ 𝑋) → ((1st ‘𝑝) ∈ (𝐹 “ 𝐴) ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = (1st ‘𝑝))) | 
| 38 |  | fvelimab 6981 | . . . . . . . 8
⊢ ((𝐹 Fn 𝑋 ∧ 𝐴 ⊆ 𝑋) → ((2nd ‘𝑝) ∈ (𝐹 “ 𝐴) ↔ ∃𝑦 ∈ 𝐴 (𝐹‘𝑦) = (2nd ‘𝑝))) | 
| 39 | 37, 38 | anbi12d 632 | . . . . . . 7
⊢ ((𝐹 Fn 𝑋 ∧ 𝐴 ⊆ 𝑋) → (((1st ‘𝑝) ∈ (𝐹 “ 𝐴) ∧ (2nd ‘𝑝) ∈ (𝐹 “ 𝐴)) ↔ (∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = (1st ‘𝑝) ∧ ∃𝑦 ∈ 𝐴 (𝐹‘𝑦) = (2nd ‘𝑝)))) | 
| 40 | 36, 39 | bitr4id 290 | . . . . . 6
⊢ ((𝐹 Fn 𝑋 ∧ 𝐴 ⊆ 𝑋) → (〈(1st ‘𝑝), (2nd ‘𝑝)〉 ∈ ran (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) ↔ ((1st ‘𝑝) ∈ (𝐹 “ 𝐴) ∧ (2nd ‘𝑝) ∈ (𝐹 “ 𝐴)))) | 
| 41 |  | opelxp 5721 | . . . . . 6
⊢
(〈(1st ‘𝑝), (2nd ‘𝑝)〉 ∈ ((𝐹 “ 𝐴) × (𝐹 “ 𝐴)) ↔ ((1st ‘𝑝) ∈ (𝐹 “ 𝐴) ∧ (2nd ‘𝑝) ∈ (𝐹 “ 𝐴))) | 
| 42 | 40, 41 | bitr4di 289 | . . . . 5
⊢ ((𝐹 Fn 𝑋 ∧ 𝐴 ⊆ 𝑋) → (〈(1st ‘𝑝), (2nd ‘𝑝)〉 ∈ ran (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) ↔ 〈(1st
‘𝑝), (2nd
‘𝑝)〉 ∈
((𝐹 “ 𝐴) × (𝐹 “ 𝐴)))) | 
| 43 | 42 | adantr 480 | . . . 4
⊢ (((𝐹 Fn 𝑋 ∧ 𝐴 ⊆ 𝑋) ∧ 𝑝 ∈ (V × V)) →
(〈(1st ‘𝑝), (2nd ‘𝑝)〉 ∈ ran (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) ↔ 〈(1st
‘𝑝), (2nd
‘𝑝)〉 ∈
((𝐹 “ 𝐴) × (𝐹 “ 𝐴)))) | 
| 44 |  | 1st2nd2 8053 | . . . . . 6
⊢ (𝑝 ∈ (V × V) →
𝑝 = 〈(1st
‘𝑝), (2nd
‘𝑝)〉) | 
| 45 | 44 | adantl 481 | . . . . 5
⊢ (((𝐹 Fn 𝑋 ∧ 𝐴 ⊆ 𝑋) ∧ 𝑝 ∈ (V × V)) → 𝑝 = 〈(1st
‘𝑝), (2nd
‘𝑝)〉) | 
| 46 | 45 | eleq1d 2826 | . . . 4
⊢ (((𝐹 Fn 𝑋 ∧ 𝐴 ⊆ 𝑋) ∧ 𝑝 ∈ (V × V)) → (𝑝 ∈ ran (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) ↔ 〈(1st
‘𝑝), (2nd
‘𝑝)〉 ∈ ran
(𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉))) | 
| 47 | 45 | eleq1d 2826 | . . . 4
⊢ (((𝐹 Fn 𝑋 ∧ 𝐴 ⊆ 𝑋) ∧ 𝑝 ∈ (V × V)) → (𝑝 ∈ ((𝐹 “ 𝐴) × (𝐹 “ 𝐴)) ↔ 〈(1st ‘𝑝), (2nd ‘𝑝)〉 ∈ ((𝐹 “ 𝐴) × (𝐹 “ 𝐴)))) | 
| 48 | 43, 46, 47 | 3bitr4d 311 | . . 3
⊢ (((𝐹 Fn 𝑋 ∧ 𝐴 ⊆ 𝑋) ∧ 𝑝 ∈ (V × V)) → (𝑝 ∈ ran (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) ↔ 𝑝 ∈ ((𝐹 “ 𝐴) × (𝐹 “ 𝐴)))) | 
| 49 | 22, 25, 48 | eqrdav 2736 | . 2
⊢ ((𝐹 Fn 𝑋 ∧ 𝐴 ⊆ 𝑋) → ran (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) = ((𝐹 “ 𝐴) × (𝐹 “ 𝐴))) | 
| 50 | 6, 49 | eqtrd 2777 | 1
⊢ ((𝐹 Fn 𝑋 ∧ 𝐴 ⊆ 𝑋) → ((𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ 〈(𝐹‘𝑥), (𝐹‘𝑦)〉) “ (𝐴 × 𝐴)) = ((𝐹 “ 𝐴) × (𝐹 “ 𝐴))) |