Step | Hyp | Ref
| Expression |
1 | | elxp6 6169 |
. . . . . . 7
⊢ (𝑧 ∈ (𝑆 × 𝑆) ↔ (𝑧 = ⟨(1st ‘𝑧), (2nd ‘𝑧)⟩ ∧ ((1st
‘𝑧) ∈ 𝑆 ∧ (2nd
‘𝑧) ∈ 𝑆))) |
2 | 1 | biimpi 120 |
. . . . . 6
⊢ (𝑧 ∈ (𝑆 × 𝑆) → (𝑧 = ⟨(1st ‘𝑧), (2nd ‘𝑧)⟩ ∧ ((1st
‘𝑧) ∈ 𝑆 ∧ (2nd
‘𝑧) ∈ 𝑆))) |
3 | 2 | adantl 277 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑆 × 𝑆)) → (𝑧 = ⟨(1st ‘𝑧), (2nd ‘𝑧)⟩ ∧ ((1st
‘𝑧) ∈ 𝑆 ∧ (2nd
‘𝑧) ∈ 𝑆))) |
4 | 3 | simpld 112 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑆 × 𝑆)) → 𝑧 = ⟨(1st ‘𝑧), (2nd ‘𝑧)⟩) |
5 | 3 | simprd 114 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑆 × 𝑆)) → ((1st ‘𝑧) ∈ 𝑆 ∧ (2nd ‘𝑧) ∈ 𝑆)) |
6 | | oprssdmm.f |
. . . . . . . . 9
⊢ (𝜑 → Rel 𝐹) |
7 | 6 | adantr 276 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → Rel 𝐹) |
8 | | eleq2 2241 |
. . . . . . . . . 10
⊢ (𝑢 = (𝐹‘⟨𝑥, 𝑦⟩) → (𝑣 ∈ 𝑢 ↔ 𝑣 ∈ (𝐹‘⟨𝑥, 𝑦⟩))) |
9 | 8 | exbidv 1825 |
. . . . . . . . 9
⊢ (𝑢 = (𝐹‘⟨𝑥, 𝑦⟩) → (∃𝑣 𝑣 ∈ 𝑢 ↔ ∃𝑣 𝑣 ∈ (𝐹‘⟨𝑥, 𝑦⟩))) |
10 | | oprssdmm.m |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑆) → ∃𝑣 𝑣 ∈ 𝑢) |
11 | 10 | ralrimiva 2550 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑢 ∈ 𝑆 ∃𝑣 𝑣 ∈ 𝑢) |
12 | 11 | adantr 276 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → ∀𝑢 ∈ 𝑆 ∃𝑣 𝑣 ∈ 𝑢) |
13 | | df-ov 5877 |
. . . . . . . . . 10
⊢ (𝑥𝐹𝑦) = (𝐹‘⟨𝑥, 𝑦⟩) |
14 | | oprssdmm.cl |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥𝐹𝑦) ∈ 𝑆) |
15 | 13, 14 | eqeltrrid 2265 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝐹‘⟨𝑥, 𝑦⟩) ∈ 𝑆) |
16 | 9, 12, 15 | rspcdva 2846 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → ∃𝑣 𝑣 ∈ (𝐹‘⟨𝑥, 𝑦⟩)) |
17 | | relelfvdm 5547 |
. . . . . . . . . 10
⊢ ((Rel
𝐹 ∧ 𝑣 ∈ (𝐹‘⟨𝑥, 𝑦⟩)) → ⟨𝑥, 𝑦⟩ ∈ dom 𝐹) |
18 | 17 | ex 115 |
. . . . . . . . 9
⊢ (Rel
𝐹 → (𝑣 ∈ (𝐹‘⟨𝑥, 𝑦⟩) → ⟨𝑥, 𝑦⟩ ∈ dom 𝐹)) |
19 | 18 | exlimdv 1819 |
. . . . . . . 8
⊢ (Rel
𝐹 → (∃𝑣 𝑣 ∈ (𝐹‘⟨𝑥, 𝑦⟩) → ⟨𝑥, 𝑦⟩ ∈ dom 𝐹)) |
20 | 7, 16, 19 | sylc 62 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → ⟨𝑥, 𝑦⟩ ∈ dom 𝐹) |
21 | 20 | ralrimivva 2559 |
. . . . . 6
⊢ (𝜑 → ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 ⟨𝑥, 𝑦⟩ ∈ dom 𝐹) |
22 | 21 | adantr 276 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑆 × 𝑆)) → ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 ⟨𝑥, 𝑦⟩ ∈ dom 𝐹) |
23 | | opeq1 3778 |
. . . . . . 7
⊢ (𝑥 = (1st ‘𝑧) → ⟨𝑥, 𝑦⟩ = ⟨(1st ‘𝑧), 𝑦⟩) |
24 | 23 | eleq1d 2246 |
. . . . . 6
⊢ (𝑥 = (1st ‘𝑧) → (⟨𝑥, 𝑦⟩ ∈ dom 𝐹 ↔ ⟨(1st ‘𝑧), 𝑦⟩ ∈ dom 𝐹)) |
25 | | opeq2 3779 |
. . . . . . 7
⊢ (𝑦 = (2nd ‘𝑧) → ⟨(1st
‘𝑧), 𝑦⟩ = ⟨(1st
‘𝑧), (2nd
‘𝑧)⟩) |
26 | 25 | eleq1d 2246 |
. . . . . 6
⊢ (𝑦 = (2nd ‘𝑧) → (⟨(1st
‘𝑧), 𝑦⟩ ∈ dom 𝐹 ↔ ⟨(1st
‘𝑧), (2nd
‘𝑧)⟩ ∈ dom
𝐹)) |
27 | 24, 26 | rspc2va 2855 |
. . . . 5
⊢
((((1st ‘𝑧) ∈ 𝑆 ∧ (2nd ‘𝑧) ∈ 𝑆) ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 ⟨𝑥, 𝑦⟩ ∈ dom 𝐹) → ⟨(1st ‘𝑧), (2nd ‘𝑧)⟩ ∈ dom 𝐹) |
28 | 5, 22, 27 | syl2anc 411 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑆 × 𝑆)) → ⟨(1st ‘𝑧), (2nd ‘𝑧)⟩ ∈ dom 𝐹) |
29 | 4, 28 | eqeltrd 2254 |
. . 3
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑆 × 𝑆)) → 𝑧 ∈ dom 𝐹) |
30 | 29 | ex 115 |
. 2
⊢ (𝜑 → (𝑧 ∈ (𝑆 × 𝑆) → 𝑧 ∈ dom 𝐹)) |
31 | 30 | ssrdv 3161 |
1
⊢ (𝜑 → (𝑆 × 𝑆) ⊆ dom 𝐹) |