Step | Hyp | Ref
| Expression |
1 | | dya2iocnrect.1 |
. . . . . 6
⊢ 𝐵 = ran (𝑒 ∈ ran (,), 𝑓 ∈ ran (,) ↦ (𝑒 × 𝑓)) |
2 | 1 | eleq2i 2824 |
. . . . 5
⊢ (𝐴 ∈ 𝐵 ↔ 𝐴 ∈ ran (𝑒 ∈ ran (,), 𝑓 ∈ ran (,) ↦ (𝑒 × 𝑓))) |
3 | | eqid 2738 |
. . . . . 6
⊢ (𝑒 ∈ ran (,), 𝑓 ∈ ran (,) ↦ (𝑒 × 𝑓)) = (𝑒 ∈ ran (,), 𝑓 ∈ ran (,) ↦ (𝑒 × 𝑓)) |
4 | | vex 3402 |
. . . . . . 7
⊢ 𝑒 ∈ V |
5 | | vex 3402 |
. . . . . . 7
⊢ 𝑓 ∈ V |
6 | 4, 5 | xpex 7494 |
. . . . . 6
⊢ (𝑒 × 𝑓) ∈ V |
7 | 3, 6 | elrnmpo 7302 |
. . . . 5
⊢ (𝐴 ∈ ran (𝑒 ∈ ran (,), 𝑓 ∈ ran (,) ↦ (𝑒 × 𝑓)) ↔ ∃𝑒 ∈ ran (,)∃𝑓 ∈ ran (,)𝐴 = (𝑒 × 𝑓)) |
8 | 2, 7 | sylbb 222 |
. . . 4
⊢ (𝐴 ∈ 𝐵 → ∃𝑒 ∈ ran (,)∃𝑓 ∈ ran (,)𝐴 = (𝑒 × 𝑓)) |
9 | 8 | 3ad2ant2 1135 |
. . 3
⊢ ((𝑋 ∈ (ℝ ×
ℝ) ∧ 𝐴 ∈
𝐵 ∧ 𝑋 ∈ 𝐴) → ∃𝑒 ∈ ran (,)∃𝑓 ∈ ran (,)𝐴 = (𝑒 × 𝑓)) |
10 | | simp1 1137 |
. . 3
⊢ ((𝑋 ∈ (ℝ ×
ℝ) ∧ 𝐴 ∈
𝐵 ∧ 𝑋 ∈ 𝐴) → 𝑋 ∈ (ℝ ×
ℝ)) |
11 | | simp3 1139 |
. . 3
⊢ ((𝑋 ∈ (ℝ ×
ℝ) ∧ 𝐴 ∈
𝐵 ∧ 𝑋 ∈ 𝐴) → 𝑋 ∈ 𝐴) |
12 | 9, 10, 11 | jca32 519 |
. 2
⊢ ((𝑋 ∈ (ℝ ×
ℝ) ∧ 𝐴 ∈
𝐵 ∧ 𝑋 ∈ 𝐴) → (∃𝑒 ∈ ran (,)∃𝑓 ∈ ran (,)𝐴 = (𝑒 × 𝑓) ∧ (𝑋 ∈ (ℝ × ℝ) ∧
𝑋 ∈ 𝐴))) |
13 | | r19.41vv 3253 |
. . 3
⊢
(∃𝑒 ∈ ran
(,)∃𝑓 ∈ ran
(,)(𝐴 = (𝑒 × 𝑓) ∧ (𝑋 ∈ (ℝ × ℝ) ∧
𝑋 ∈ 𝐴)) ↔ (∃𝑒 ∈ ran (,)∃𝑓 ∈ ran (,)𝐴 = (𝑒 × 𝑓) ∧ (𝑋 ∈ (ℝ × ℝ) ∧
𝑋 ∈ 𝐴))) |
14 | 13 | biimpri 231 |
. 2
⊢
((∃𝑒 ∈
ran (,)∃𝑓 ∈ ran
(,)𝐴 = (𝑒 × 𝑓) ∧ (𝑋 ∈ (ℝ × ℝ) ∧
𝑋 ∈ 𝐴)) → ∃𝑒 ∈ ran (,)∃𝑓 ∈ ran (,)(𝐴 = (𝑒 × 𝑓) ∧ (𝑋 ∈ (ℝ × ℝ) ∧
𝑋 ∈ 𝐴))) |
15 | | simprl 771 |
. . . . . 6
⊢ ((𝐴 = (𝑒 × 𝑓) ∧ (𝑋 ∈ (ℝ × ℝ) ∧
𝑋 ∈ 𝐴)) → 𝑋 ∈ (ℝ ×
ℝ)) |
16 | | simpl 486 |
. . . . . 6
⊢ ((𝐴 = (𝑒 × 𝑓) ∧ (𝑋 ∈ (ℝ × ℝ) ∧
𝑋 ∈ 𝐴)) → 𝐴 = (𝑒 × 𝑓)) |
17 | | simprr 773 |
. . . . . . 7
⊢ ((𝐴 = (𝑒 × 𝑓) ∧ (𝑋 ∈ (ℝ × ℝ) ∧
𝑋 ∈ 𝐴)) → 𝑋 ∈ 𝐴) |
18 | 17, 16 | eleqtrd 2835 |
. . . . . 6
⊢ ((𝐴 = (𝑒 × 𝑓) ∧ (𝑋 ∈ (ℝ × ℝ) ∧
𝑋 ∈ 𝐴)) → 𝑋 ∈ (𝑒 × 𝑓)) |
19 | 15, 16, 18 | 3jca 1129 |
. . . . 5
⊢ ((𝐴 = (𝑒 × 𝑓) ∧ (𝑋 ∈ (ℝ × ℝ) ∧
𝑋 ∈ 𝐴)) → (𝑋 ∈ (ℝ × ℝ) ∧
𝐴 = (𝑒 × 𝑓) ∧ 𝑋 ∈ (𝑒 × 𝑓))) |
20 | | simpr 488 |
. . . . . 6
⊢ (((𝑒 ∈ ran (,) ∧ 𝑓 ∈ ran (,)) ∧ (𝑋 ∈ (ℝ ×
ℝ) ∧ 𝐴 = (𝑒 × 𝑓) ∧ 𝑋 ∈ (𝑒 × 𝑓))) → (𝑋 ∈ (ℝ × ℝ) ∧
𝐴 = (𝑒 × 𝑓) ∧ 𝑋 ∈ (𝑒 × 𝑓))) |
21 | | xp1st 7746 |
. . . . . . . . . 10
⊢ (𝑋 ∈ (ℝ ×
ℝ) → (1st ‘𝑋) ∈ ℝ) |
22 | 21 | 3ad2ant1 1134 |
. . . . . . . . 9
⊢ ((𝑋 ∈ (ℝ ×
ℝ) ∧ 𝐴 = (𝑒 × 𝑓) ∧ 𝑋 ∈ (𝑒 × 𝑓)) → (1st ‘𝑋) ∈
ℝ) |
23 | 22 | adantl 485 |
. . . . . . . 8
⊢ (((𝑒 ∈ ran (,) ∧ 𝑓 ∈ ran (,)) ∧ (𝑋 ∈ (ℝ ×
ℝ) ∧ 𝐴 = (𝑒 × 𝑓) ∧ 𝑋 ∈ (𝑒 × 𝑓))) → (1st ‘𝑋) ∈
ℝ) |
24 | | simpll 767 |
. . . . . . . 8
⊢ (((𝑒 ∈ ran (,) ∧ 𝑓 ∈ ran (,)) ∧ (𝑋 ∈ (ℝ ×
ℝ) ∧ 𝐴 = (𝑒 × 𝑓) ∧ 𝑋 ∈ (𝑒 × 𝑓))) → 𝑒 ∈ ran (,)) |
25 | | xp1st 7746 |
. . . . . . . . . 10
⊢ (𝑋 ∈ (𝑒 × 𝑓) → (1st ‘𝑋) ∈ 𝑒) |
26 | 25 | 3ad2ant3 1136 |
. . . . . . . . 9
⊢ ((𝑋 ∈ (ℝ ×
ℝ) ∧ 𝐴 = (𝑒 × 𝑓) ∧ 𝑋 ∈ (𝑒 × 𝑓)) → (1st ‘𝑋) ∈ 𝑒) |
27 | 26 | adantl 485 |
. . . . . . . 8
⊢ (((𝑒 ∈ ran (,) ∧ 𝑓 ∈ ran (,)) ∧ (𝑋 ∈ (ℝ ×
ℝ) ∧ 𝐴 = (𝑒 × 𝑓) ∧ 𝑋 ∈ (𝑒 × 𝑓))) → (1st ‘𝑋) ∈ 𝑒) |
28 | | sxbrsiga.0 |
. . . . . . . . 9
⊢ 𝐽 = (topGen‘ran
(,)) |
29 | | dya2ioc.1 |
. . . . . . . . 9
⊢ 𝐼 = (𝑥 ∈ ℤ, 𝑛 ∈ ℤ ↦ ((𝑥 / (2↑𝑛))[,)((𝑥 + 1) / (2↑𝑛)))) |
30 | 28, 29 | dya2icoseg2 31815 |
. . . . . . . 8
⊢
(((1st ‘𝑋) ∈ ℝ ∧ 𝑒 ∈ ran (,) ∧ (1st
‘𝑋) ∈ 𝑒) → ∃𝑠 ∈ ran 𝐼((1st ‘𝑋) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑒)) |
31 | 23, 24, 27, 30 | syl3anc 1372 |
. . . . . . 7
⊢ (((𝑒 ∈ ran (,) ∧ 𝑓 ∈ ran (,)) ∧ (𝑋 ∈ (ℝ ×
ℝ) ∧ 𝐴 = (𝑒 × 𝑓) ∧ 𝑋 ∈ (𝑒 × 𝑓))) → ∃𝑠 ∈ ran 𝐼((1st ‘𝑋) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑒)) |
32 | | xp2nd 7747 |
. . . . . . . . . 10
⊢ (𝑋 ∈ (ℝ ×
ℝ) → (2nd ‘𝑋) ∈ ℝ) |
33 | 32 | 3ad2ant1 1134 |
. . . . . . . . 9
⊢ ((𝑋 ∈ (ℝ ×
ℝ) ∧ 𝐴 = (𝑒 × 𝑓) ∧ 𝑋 ∈ (𝑒 × 𝑓)) → (2nd ‘𝑋) ∈
ℝ) |
34 | 33 | adantl 485 |
. . . . . . . 8
⊢ (((𝑒 ∈ ran (,) ∧ 𝑓 ∈ ran (,)) ∧ (𝑋 ∈ (ℝ ×
ℝ) ∧ 𝐴 = (𝑒 × 𝑓) ∧ 𝑋 ∈ (𝑒 × 𝑓))) → (2nd ‘𝑋) ∈
ℝ) |
35 | | simplr 769 |
. . . . . . . 8
⊢ (((𝑒 ∈ ran (,) ∧ 𝑓 ∈ ran (,)) ∧ (𝑋 ∈ (ℝ ×
ℝ) ∧ 𝐴 = (𝑒 × 𝑓) ∧ 𝑋 ∈ (𝑒 × 𝑓))) → 𝑓 ∈ ran (,)) |
36 | | xp2nd 7747 |
. . . . . . . . . 10
⊢ (𝑋 ∈ (𝑒 × 𝑓) → (2nd ‘𝑋) ∈ 𝑓) |
37 | 36 | 3ad2ant3 1136 |
. . . . . . . . 9
⊢ ((𝑋 ∈ (ℝ ×
ℝ) ∧ 𝐴 = (𝑒 × 𝑓) ∧ 𝑋 ∈ (𝑒 × 𝑓)) → (2nd ‘𝑋) ∈ 𝑓) |
38 | 37 | adantl 485 |
. . . . . . . 8
⊢ (((𝑒 ∈ ran (,) ∧ 𝑓 ∈ ran (,)) ∧ (𝑋 ∈ (ℝ ×
ℝ) ∧ 𝐴 = (𝑒 × 𝑓) ∧ 𝑋 ∈ (𝑒 × 𝑓))) → (2nd ‘𝑋) ∈ 𝑓) |
39 | 28, 29 | dya2icoseg2 31815 |
. . . . . . . 8
⊢
(((2nd ‘𝑋) ∈ ℝ ∧ 𝑓 ∈ ran (,) ∧ (2nd
‘𝑋) ∈ 𝑓) → ∃𝑡 ∈ ran 𝐼((2nd ‘𝑋) ∈ 𝑡 ∧ 𝑡 ⊆ 𝑓)) |
40 | 34, 35, 38, 39 | syl3anc 1372 |
. . . . . . 7
⊢ (((𝑒 ∈ ran (,) ∧ 𝑓 ∈ ran (,)) ∧ (𝑋 ∈ (ℝ ×
ℝ) ∧ 𝐴 = (𝑒 × 𝑓) ∧ 𝑋 ∈ (𝑒 × 𝑓))) → ∃𝑡 ∈ ran 𝐼((2nd ‘𝑋) ∈ 𝑡 ∧ 𝑡 ⊆ 𝑓)) |
41 | | reeanv 3270 |
. . . . . . 7
⊢
(∃𝑠 ∈ ran
𝐼∃𝑡 ∈ ran 𝐼(((1st ‘𝑋) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑒) ∧ ((2nd ‘𝑋) ∈ 𝑡 ∧ 𝑡 ⊆ 𝑓)) ↔ (∃𝑠 ∈ ran 𝐼((1st ‘𝑋) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑒) ∧ ∃𝑡 ∈ ran 𝐼((2nd ‘𝑋) ∈ 𝑡 ∧ 𝑡 ⊆ 𝑓))) |
42 | 31, 40, 41 | sylanbrc 586 |
. . . . . 6
⊢ (((𝑒 ∈ ran (,) ∧ 𝑓 ∈ ran (,)) ∧ (𝑋 ∈ (ℝ ×
ℝ) ∧ 𝐴 = (𝑒 × 𝑓) ∧ 𝑋 ∈ (𝑒 × 𝑓))) → ∃𝑠 ∈ ran 𝐼∃𝑡 ∈ ran 𝐼(((1st ‘𝑋) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑒) ∧ ((2nd ‘𝑋) ∈ 𝑡 ∧ 𝑡 ⊆ 𝑓))) |
43 | | eqid 2738 |
. . . . . . . . . . . 12
⊢ (𝑠 × 𝑡) = (𝑠 × 𝑡) |
44 | | xpeq1 5539 |
. . . . . . . . . . . . . 14
⊢ (𝑢 = 𝑠 → (𝑢 × 𝑣) = (𝑠 × 𝑣)) |
45 | 44 | eqeq2d 2749 |
. . . . . . . . . . . . 13
⊢ (𝑢 = 𝑠 → ((𝑠 × 𝑡) = (𝑢 × 𝑣) ↔ (𝑠 × 𝑡) = (𝑠 × 𝑣))) |
46 | | xpeq2 5546 |
. . . . . . . . . . . . . 14
⊢ (𝑣 = 𝑡 → (𝑠 × 𝑣) = (𝑠 × 𝑡)) |
47 | 46 | eqeq2d 2749 |
. . . . . . . . . . . . 13
⊢ (𝑣 = 𝑡 → ((𝑠 × 𝑡) = (𝑠 × 𝑣) ↔ (𝑠 × 𝑡) = (𝑠 × 𝑡))) |
48 | 45, 47 | rspc2ev 3538 |
. . . . . . . . . . . 12
⊢ ((𝑠 ∈ ran 𝐼 ∧ 𝑡 ∈ ran 𝐼 ∧ (𝑠 × 𝑡) = (𝑠 × 𝑡)) → ∃𝑢 ∈ ran 𝐼∃𝑣 ∈ ran 𝐼(𝑠 × 𝑡) = (𝑢 × 𝑣)) |
49 | 43, 48 | mp3an3 1451 |
. . . . . . . . . . 11
⊢ ((𝑠 ∈ ran 𝐼 ∧ 𝑡 ∈ ran 𝐼) → ∃𝑢 ∈ ran 𝐼∃𝑣 ∈ ran 𝐼(𝑠 × 𝑡) = (𝑢 × 𝑣)) |
50 | | dya2ioc.2 |
. . . . . . . . . . . 12
⊢ 𝑅 = (𝑢 ∈ ran 𝐼, 𝑣 ∈ ran 𝐼 ↦ (𝑢 × 𝑣)) |
51 | | vex 3402 |
. . . . . . . . . . . . 13
⊢ 𝑢 ∈ V |
52 | | vex 3402 |
. . . . . . . . . . . . 13
⊢ 𝑣 ∈ V |
53 | 51, 52 | xpex 7494 |
. . . . . . . . . . . 12
⊢ (𝑢 × 𝑣) ∈ V |
54 | 50, 53 | elrnmpo 7302 |
. . . . . . . . . . 11
⊢ ((𝑠 × 𝑡) ∈ ran 𝑅 ↔ ∃𝑢 ∈ ran 𝐼∃𝑣 ∈ ran 𝐼(𝑠 × 𝑡) = (𝑢 × 𝑣)) |
55 | 49, 54 | sylibr 237 |
. . . . . . . . . 10
⊢ ((𝑠 ∈ ran 𝐼 ∧ 𝑡 ∈ ran 𝐼) → (𝑠 × 𝑡) ∈ ran 𝑅) |
56 | 55 | ad2antrl 728 |
. . . . . . . . 9
⊢ (((𝑋 ∈ (ℝ ×
ℝ) ∧ 𝐴 = (𝑒 × 𝑓) ∧ 𝑋 ∈ (𝑒 × 𝑓)) ∧ ((𝑠 ∈ ran 𝐼 ∧ 𝑡 ∈ ran 𝐼) ∧ (((1st ‘𝑋) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑒) ∧ ((2nd ‘𝑋) ∈ 𝑡 ∧ 𝑡 ⊆ 𝑓)))) → (𝑠 × 𝑡) ∈ ran 𝑅) |
57 | | xpss 5541 |
. . . . . . . . . . 11
⊢ (ℝ
× ℝ) ⊆ (V × V) |
58 | | simpl1 1192 |
. . . . . . . . . . 11
⊢ (((𝑋 ∈ (ℝ ×
ℝ) ∧ 𝐴 = (𝑒 × 𝑓) ∧ 𝑋 ∈ (𝑒 × 𝑓)) ∧ ((𝑠 ∈ ran 𝐼 ∧ 𝑡 ∈ ran 𝐼) ∧ (((1st ‘𝑋) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑒) ∧ ((2nd ‘𝑋) ∈ 𝑡 ∧ 𝑡 ⊆ 𝑓)))) → 𝑋 ∈ (ℝ ×
ℝ)) |
59 | 57, 58 | sseldi 3875 |
. . . . . . . . . 10
⊢ (((𝑋 ∈ (ℝ ×
ℝ) ∧ 𝐴 = (𝑒 × 𝑓) ∧ 𝑋 ∈ (𝑒 × 𝑓)) ∧ ((𝑠 ∈ ran 𝐼 ∧ 𝑡 ∈ ran 𝐼) ∧ (((1st ‘𝑋) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑒) ∧ ((2nd ‘𝑋) ∈ 𝑡 ∧ 𝑡 ⊆ 𝑓)))) → 𝑋 ∈ (V × V)) |
60 | | simprrl 781 |
. . . . . . . . . . 11
⊢ (((𝑋 ∈ (ℝ ×
ℝ) ∧ 𝐴 = (𝑒 × 𝑓) ∧ 𝑋 ∈ (𝑒 × 𝑓)) ∧ ((𝑠 ∈ ran 𝐼 ∧ 𝑡 ∈ ran 𝐼) ∧ (((1st ‘𝑋) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑒) ∧ ((2nd ‘𝑋) ∈ 𝑡 ∧ 𝑡 ⊆ 𝑓)))) → ((1st ‘𝑋) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑒)) |
61 | 60 | simpld 498 |
. . . . . . . . . 10
⊢ (((𝑋 ∈ (ℝ ×
ℝ) ∧ 𝐴 = (𝑒 × 𝑓) ∧ 𝑋 ∈ (𝑒 × 𝑓)) ∧ ((𝑠 ∈ ran 𝐼 ∧ 𝑡 ∈ ran 𝐼) ∧ (((1st ‘𝑋) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑒) ∧ ((2nd ‘𝑋) ∈ 𝑡 ∧ 𝑡 ⊆ 𝑓)))) → (1st ‘𝑋) ∈ 𝑠) |
62 | | simprrr 782 |
. . . . . . . . . . 11
⊢ (((𝑋 ∈ (ℝ ×
ℝ) ∧ 𝐴 = (𝑒 × 𝑓) ∧ 𝑋 ∈ (𝑒 × 𝑓)) ∧ ((𝑠 ∈ ran 𝐼 ∧ 𝑡 ∈ ran 𝐼) ∧ (((1st ‘𝑋) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑒) ∧ ((2nd ‘𝑋) ∈ 𝑡 ∧ 𝑡 ⊆ 𝑓)))) → ((2nd ‘𝑋) ∈ 𝑡 ∧ 𝑡 ⊆ 𝑓)) |
63 | 62 | simpld 498 |
. . . . . . . . . 10
⊢ (((𝑋 ∈ (ℝ ×
ℝ) ∧ 𝐴 = (𝑒 × 𝑓) ∧ 𝑋 ∈ (𝑒 × 𝑓)) ∧ ((𝑠 ∈ ran 𝐼 ∧ 𝑡 ∈ ran 𝐼) ∧ (((1st ‘𝑋) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑒) ∧ ((2nd ‘𝑋) ∈ 𝑡 ∧ 𝑡 ⊆ 𝑓)))) → (2nd ‘𝑋) ∈ 𝑡) |
64 | | elxp7 7749 |
. . . . . . . . . . 11
⊢ (𝑋 ∈ (𝑠 × 𝑡) ↔ (𝑋 ∈ (V × V) ∧ ((1st
‘𝑋) ∈ 𝑠 ∧ (2nd
‘𝑋) ∈ 𝑡))) |
65 | 64 | biimpri 231 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ (V × V) ∧
((1st ‘𝑋)
∈ 𝑠 ∧
(2nd ‘𝑋)
∈ 𝑡)) → 𝑋 ∈ (𝑠 × 𝑡)) |
66 | 59, 61, 63, 65 | syl12anc 836 |
. . . . . . . . 9
⊢ (((𝑋 ∈ (ℝ ×
ℝ) ∧ 𝐴 = (𝑒 × 𝑓) ∧ 𝑋 ∈ (𝑒 × 𝑓)) ∧ ((𝑠 ∈ ran 𝐼 ∧ 𝑡 ∈ ran 𝐼) ∧ (((1st ‘𝑋) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑒) ∧ ((2nd ‘𝑋) ∈ 𝑡 ∧ 𝑡 ⊆ 𝑓)))) → 𝑋 ∈ (𝑠 × 𝑡)) |
67 | 60 | simprd 499 |
. . . . . . . . . . 11
⊢ (((𝑋 ∈ (ℝ ×
ℝ) ∧ 𝐴 = (𝑒 × 𝑓) ∧ 𝑋 ∈ (𝑒 × 𝑓)) ∧ ((𝑠 ∈ ran 𝐼 ∧ 𝑡 ∈ ran 𝐼) ∧ (((1st ‘𝑋) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑒) ∧ ((2nd ‘𝑋) ∈ 𝑡 ∧ 𝑡 ⊆ 𝑓)))) → 𝑠 ⊆ 𝑒) |
68 | 62 | simprd 499 |
. . . . . . . . . . 11
⊢ (((𝑋 ∈ (ℝ ×
ℝ) ∧ 𝐴 = (𝑒 × 𝑓) ∧ 𝑋 ∈ (𝑒 × 𝑓)) ∧ ((𝑠 ∈ ran 𝐼 ∧ 𝑡 ∈ ran 𝐼) ∧ (((1st ‘𝑋) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑒) ∧ ((2nd ‘𝑋) ∈ 𝑡 ∧ 𝑡 ⊆ 𝑓)))) → 𝑡 ⊆ 𝑓) |
69 | | xpss12 5540 |
. . . . . . . . . . 11
⊢ ((𝑠 ⊆ 𝑒 ∧ 𝑡 ⊆ 𝑓) → (𝑠 × 𝑡) ⊆ (𝑒 × 𝑓)) |
70 | 67, 68, 69 | syl2anc 587 |
. . . . . . . . . 10
⊢ (((𝑋 ∈ (ℝ ×
ℝ) ∧ 𝐴 = (𝑒 × 𝑓) ∧ 𝑋 ∈ (𝑒 × 𝑓)) ∧ ((𝑠 ∈ ran 𝐼 ∧ 𝑡 ∈ ran 𝐼) ∧ (((1st ‘𝑋) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑒) ∧ ((2nd ‘𝑋) ∈ 𝑡 ∧ 𝑡 ⊆ 𝑓)))) → (𝑠 × 𝑡) ⊆ (𝑒 × 𝑓)) |
71 | | simpl2 1193 |
. . . . . . . . . 10
⊢ (((𝑋 ∈ (ℝ ×
ℝ) ∧ 𝐴 = (𝑒 × 𝑓) ∧ 𝑋 ∈ (𝑒 × 𝑓)) ∧ ((𝑠 ∈ ran 𝐼 ∧ 𝑡 ∈ ran 𝐼) ∧ (((1st ‘𝑋) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑒) ∧ ((2nd ‘𝑋) ∈ 𝑡 ∧ 𝑡 ⊆ 𝑓)))) → 𝐴 = (𝑒 × 𝑓)) |
72 | 70, 71 | sseqtrrd 3918 |
. . . . . . . . 9
⊢ (((𝑋 ∈ (ℝ ×
ℝ) ∧ 𝐴 = (𝑒 × 𝑓) ∧ 𝑋 ∈ (𝑒 × 𝑓)) ∧ ((𝑠 ∈ ran 𝐼 ∧ 𝑡 ∈ ran 𝐼) ∧ (((1st ‘𝑋) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑒) ∧ ((2nd ‘𝑋) ∈ 𝑡 ∧ 𝑡 ⊆ 𝑓)))) → (𝑠 × 𝑡) ⊆ 𝐴) |
73 | | eleq2 2821 |
. . . . . . . . . . 11
⊢ (𝑏 = (𝑠 × 𝑡) → (𝑋 ∈ 𝑏 ↔ 𝑋 ∈ (𝑠 × 𝑡))) |
74 | | sseq1 3902 |
. . . . . . . . . . 11
⊢ (𝑏 = (𝑠 × 𝑡) → (𝑏 ⊆ 𝐴 ↔ (𝑠 × 𝑡) ⊆ 𝐴)) |
75 | 73, 74 | anbi12d 634 |
. . . . . . . . . 10
⊢ (𝑏 = (𝑠 × 𝑡) → ((𝑋 ∈ 𝑏 ∧ 𝑏 ⊆ 𝐴) ↔ (𝑋 ∈ (𝑠 × 𝑡) ∧ (𝑠 × 𝑡) ⊆ 𝐴))) |
76 | 75 | rspcev 3526 |
. . . . . . . . 9
⊢ (((𝑠 × 𝑡) ∈ ran 𝑅 ∧ (𝑋 ∈ (𝑠 × 𝑡) ∧ (𝑠 × 𝑡) ⊆ 𝐴)) → ∃𝑏 ∈ ran 𝑅(𝑋 ∈ 𝑏 ∧ 𝑏 ⊆ 𝐴)) |
77 | 56, 66, 72, 76 | syl12anc 836 |
. . . . . . . 8
⊢ (((𝑋 ∈ (ℝ ×
ℝ) ∧ 𝐴 = (𝑒 × 𝑓) ∧ 𝑋 ∈ (𝑒 × 𝑓)) ∧ ((𝑠 ∈ ran 𝐼 ∧ 𝑡 ∈ ran 𝐼) ∧ (((1st ‘𝑋) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑒) ∧ ((2nd ‘𝑋) ∈ 𝑡 ∧ 𝑡 ⊆ 𝑓)))) → ∃𝑏 ∈ ran 𝑅(𝑋 ∈ 𝑏 ∧ 𝑏 ⊆ 𝐴)) |
78 | 77 | exp32 424 |
. . . . . . 7
⊢ ((𝑋 ∈ (ℝ ×
ℝ) ∧ 𝐴 = (𝑒 × 𝑓) ∧ 𝑋 ∈ (𝑒 × 𝑓)) → ((𝑠 ∈ ran 𝐼 ∧ 𝑡 ∈ ran 𝐼) → ((((1st ‘𝑋) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑒) ∧ ((2nd ‘𝑋) ∈ 𝑡 ∧ 𝑡 ⊆ 𝑓)) → ∃𝑏 ∈ ran 𝑅(𝑋 ∈ 𝑏 ∧ 𝑏 ⊆ 𝐴)))) |
79 | 78 | rexlimdvv 3203 |
. . . . . 6
⊢ ((𝑋 ∈ (ℝ ×
ℝ) ∧ 𝐴 = (𝑒 × 𝑓) ∧ 𝑋 ∈ (𝑒 × 𝑓)) → (∃𝑠 ∈ ran 𝐼∃𝑡 ∈ ran 𝐼(((1st ‘𝑋) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑒) ∧ ((2nd ‘𝑋) ∈ 𝑡 ∧ 𝑡 ⊆ 𝑓)) → ∃𝑏 ∈ ran 𝑅(𝑋 ∈ 𝑏 ∧ 𝑏 ⊆ 𝐴))) |
80 | 20, 42, 79 | sylc 65 |
. . . . 5
⊢ (((𝑒 ∈ ran (,) ∧ 𝑓 ∈ ran (,)) ∧ (𝑋 ∈ (ℝ ×
ℝ) ∧ 𝐴 = (𝑒 × 𝑓) ∧ 𝑋 ∈ (𝑒 × 𝑓))) → ∃𝑏 ∈ ran 𝑅(𝑋 ∈ 𝑏 ∧ 𝑏 ⊆ 𝐴)) |
81 | 19, 80 | sylan2 596 |
. . . 4
⊢ (((𝑒 ∈ ran (,) ∧ 𝑓 ∈ ran (,)) ∧ (𝐴 = (𝑒 × 𝑓) ∧ (𝑋 ∈ (ℝ × ℝ) ∧
𝑋 ∈ 𝐴))) → ∃𝑏 ∈ ran 𝑅(𝑋 ∈ 𝑏 ∧ 𝑏 ⊆ 𝐴)) |
82 | 81 | ex 416 |
. . 3
⊢ ((𝑒 ∈ ran (,) ∧ 𝑓 ∈ ran (,)) → ((𝐴 = (𝑒 × 𝑓) ∧ (𝑋 ∈ (ℝ × ℝ) ∧
𝑋 ∈ 𝐴)) → ∃𝑏 ∈ ran 𝑅(𝑋 ∈ 𝑏 ∧ 𝑏 ⊆ 𝐴))) |
83 | 82 | rexlimivv 3202 |
. 2
⊢
(∃𝑒 ∈ ran
(,)∃𝑓 ∈ ran
(,)(𝐴 = (𝑒 × 𝑓) ∧ (𝑋 ∈ (ℝ × ℝ) ∧
𝑋 ∈ 𝐴)) → ∃𝑏 ∈ ran 𝑅(𝑋 ∈ 𝑏 ∧ 𝑏 ⊆ 𝐴)) |
84 | 12, 14, 83 | 3syl 18 |
1
⊢ ((𝑋 ∈ (ℝ ×
ℝ) ∧ 𝐴 ∈
𝐵 ∧ 𝑋 ∈ 𝐴) → ∃𝑏 ∈ ran 𝑅(𝑋 ∈ 𝑏 ∧ 𝑏 ⊆ 𝐴)) |