Metamath Proof Explorer

Theorem dya2iocnrect

Description: For any point of an open rectangle in ( RR X. RR ) , there is a closed-below open-above dyadic rational square which contains that point and is included in the rectangle. (Contributed by Thierry Arnoux, 12-Oct-2017)

Ref Expression
Hypotheses sxbrsiga.0 ⊢ 𝐽 = ( topGen ‘ ran (,) )
dya2ioc.1 ⊢ 𝐼 = ( 𝑥 ∈ ℤ , 𝑛 ∈ ℤ ↦ ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) )
dya2ioc.2 ⊢ 𝑅 = ( 𝑢 ∈ ran 𝐼 , 𝑣 ∈ ran 𝐼 ↦ ( 𝑢 × 𝑣 ) )
dya2iocnrect.1 ⊢ 𝐵 = ran ( 𝑒 ∈ ran (,) , 𝑓 ∈ ran (,) ↦ ( 𝑒 × 𝑓 ) )
Assertion dya2iocnrect ( ( 𝑋 ∈ ( ℝ × ℝ ) ∧ 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝐴 ) → ∃ 𝑏 ∈ ran 𝑅 ( 𝑋 ∈ 𝑏 ∧ 𝑏 ⊆ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 sxbrsiga.0 ⊢ 𝐽 = ( topGen ‘ ran (,) )
2 dya2ioc.1 ⊢ 𝐼 = ( 𝑥 ∈ ℤ , 𝑛 ∈ ℤ ↦ ( ( 𝑥 / ( 2 ↑ 𝑛 ) ) [,) ( ( 𝑥 + 1 ) / ( 2 ↑ 𝑛 ) ) ) )
3 dya2ioc.2 ⊢ 𝑅 = ( 𝑢 ∈ ran 𝐼 , 𝑣 ∈ ran 𝐼 ↦ ( 𝑢 × 𝑣 ) )
4 dya2iocnrect.1 ⊢ 𝐵 = ran ( 𝑒 ∈ ran (,) , 𝑓 ∈ ran (,) ↦ ( 𝑒 × 𝑓 ) )
5 4 eleq2i ⊢ ( 𝐴 ∈ 𝐵 ↔ 𝐴 ∈ ran ( 𝑒 ∈ ran (,) , 𝑓 ∈ ran (,) ↦ ( 𝑒 × 𝑓 ) ) )
6 eqid ⊢ ( 𝑒 ∈ ran (,) , 𝑓 ∈ ran (,) ↦ ( 𝑒 × 𝑓 ) ) = ( 𝑒 ∈ ran (,) , 𝑓 ∈ ran (,) ↦ ( 𝑒 × 𝑓 ) )
7 vex ⊢ 𝑒 ∈ V
8 vex ⊢ 𝑓 ∈ V
9 7 8 xpex ⊢ ( 𝑒 × 𝑓 ) ∈ V
10 6 9 elrnmpo ⊢ ( 𝐴 ∈ ran ( 𝑒 ∈ ran (,) , 𝑓 ∈ ran (,) ↦ ( 𝑒 × 𝑓 ) ) ↔ ∃ 𝑒 ∈ ran (,) ∃ 𝑓 ∈ ran (,) 𝐴 = ( 𝑒 × 𝑓 ) )
11 5 10 sylbb ⊢ ( 𝐴 ∈ 𝐵 → ∃ 𝑒 ∈ ran (,) ∃ 𝑓 ∈ ran (,) 𝐴 = ( 𝑒 × 𝑓 ) )
12 11 3ad2ant2 ⊢ ( ( 𝑋 ∈ ( ℝ × ℝ ) ∧ 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝐴 ) → ∃ 𝑒 ∈ ran (,) ∃ 𝑓 ∈ ran (,) 𝐴 = ( 𝑒 × 𝑓 ) )
13 simp1 ⊢ ( ( 𝑋 ∈ ( ℝ × ℝ ) ∧ 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝐴 ) → 𝑋 ∈ ( ℝ × ℝ ) )
14 simp3 ⊢ ( ( 𝑋 ∈ ( ℝ × ℝ ) ∧ 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝐴 ) → 𝑋 ∈ 𝐴 )
15 12 13 14 jca32 ⊢ ( ( 𝑋 ∈ ( ℝ × ℝ ) ∧ 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝐴 ) → ( ∃ 𝑒 ∈ ran (,) ∃ 𝑓 ∈ ran (,) 𝐴 = ( 𝑒 × 𝑓 ) ∧ ( 𝑋 ∈ ( ℝ × ℝ ) ∧ 𝑋 ∈ 𝐴 ) ) )
16 r19.41vv ⊢ ( ∃ 𝑒 ∈ ran (,) ∃ 𝑓 ∈ ran (,) ( 𝐴 = ( 𝑒 × 𝑓 ) ∧ ( 𝑋 ∈ ( ℝ × ℝ ) ∧ 𝑋 ∈ 𝐴 ) ) ↔ ( ∃ 𝑒 ∈ ran (,) ∃ 𝑓 ∈ ran (,) 𝐴 = ( 𝑒 × 𝑓 ) ∧ ( 𝑋 ∈ ( ℝ × ℝ ) ∧ 𝑋 ∈ 𝐴 ) ) )
17 16 biimpri ⊢ ( ( ∃ 𝑒 ∈ ran (,) ∃ 𝑓 ∈ ran (,) 𝐴 = ( 𝑒 × 𝑓 ) ∧ ( 𝑋 ∈ ( ℝ × ℝ ) ∧ 𝑋 ∈ 𝐴 ) ) → ∃ 𝑒 ∈ ran (,) ∃ 𝑓 ∈ ran (,) ( 𝐴 = ( 𝑒 × 𝑓 ) ∧ ( 𝑋 ∈ ( ℝ × ℝ ) ∧ 𝑋 ∈ 𝐴 ) ) )
18 simprl ⊢ ( ( 𝐴 = ( 𝑒 × 𝑓 ) ∧ ( 𝑋 ∈ ( ℝ × ℝ ) ∧ 𝑋 ∈ 𝐴 ) ) → 𝑋 ∈ ( ℝ × ℝ ) )
19 simpl ⊢ ( ( 𝐴 = ( 𝑒 × 𝑓 ) ∧ ( 𝑋 ∈ ( ℝ × ℝ ) ∧ 𝑋 ∈ 𝐴 ) ) → 𝐴 = ( 𝑒 × 𝑓 ) )
20 simprr ⊢ ( ( 𝐴 = ( 𝑒 × 𝑓 ) ∧ ( 𝑋 ∈ ( ℝ × ℝ ) ∧ 𝑋 ∈ 𝐴 ) ) → 𝑋 ∈ 𝐴 )
21 20 19 eleqtrd ⊢ ( ( 𝐴 = ( 𝑒 × 𝑓 ) ∧ ( 𝑋 ∈ ( ℝ × ℝ ) ∧ 𝑋 ∈ 𝐴 ) ) → 𝑋 ∈ ( 𝑒 × 𝑓 ) )
22 18 19 21 3jca ⊢ ( ( 𝐴 = ( 𝑒 × 𝑓 ) ∧ ( 𝑋 ∈ ( ℝ × ℝ ) ∧ 𝑋 ∈ 𝐴 ) ) → ( 𝑋 ∈ ( ℝ × ℝ ) ∧ 𝐴 = ( 𝑒 × 𝑓 ) ∧ 𝑋 ∈ ( 𝑒 × 𝑓 ) ) )
23 simpr ⊢ ( ( ( 𝑒 ∈ ran (,) ∧ 𝑓 ∈ ran (,) ) ∧ ( 𝑋 ∈ ( ℝ × ℝ ) ∧ 𝐴 = ( 𝑒 × 𝑓 ) ∧ 𝑋 ∈ ( 𝑒 × 𝑓 ) ) ) → ( 𝑋 ∈ ( ℝ × ℝ ) ∧ 𝐴 = ( 𝑒 × 𝑓 ) ∧ 𝑋 ∈ ( 𝑒 × 𝑓 ) ) )
24 xp1st ⊢ ( 𝑋 ∈ ( ℝ × ℝ ) → ( 1st ‘ 𝑋 ) ∈ ℝ )
25 24 3ad2ant1 ⊢ ( ( 𝑋 ∈ ( ℝ × ℝ ) ∧ 𝐴 = ( 𝑒 × 𝑓 ) ∧ 𝑋 ∈ ( 𝑒 × 𝑓 ) ) → ( 1st ‘ 𝑋 ) ∈ ℝ )
26 25 adantl ⊢ ( ( ( 𝑒 ∈ ran (,) ∧ 𝑓 ∈ ran (,) ) ∧ ( 𝑋 ∈ ( ℝ × ℝ ) ∧ 𝐴 = ( 𝑒 × 𝑓 ) ∧ 𝑋 ∈ ( 𝑒 × 𝑓 ) ) ) → ( 1st ‘ 𝑋 ) ∈ ℝ )
27 simpll ⊢ ( ( ( 𝑒 ∈ ran (,) ∧ 𝑓 ∈ ran (,) ) ∧ ( 𝑋 ∈ ( ℝ × ℝ ) ∧ 𝐴 = ( 𝑒 × 𝑓 ) ∧ 𝑋 ∈ ( 𝑒 × 𝑓 ) ) ) → 𝑒 ∈ ran (,) )
28 xp1st ⊢ ( 𝑋 ∈ ( 𝑒 × 𝑓 ) → ( 1st ‘ 𝑋 ) ∈ 𝑒 )
29 28 3ad2ant3 ⊢ ( ( 𝑋 ∈ ( ℝ × ℝ ) ∧ 𝐴 = ( 𝑒 × 𝑓 ) ∧ 𝑋 ∈ ( 𝑒 × 𝑓 ) ) → ( 1st ‘ 𝑋 ) ∈ 𝑒 )
30 29 adantl ⊢ ( ( ( 𝑒 ∈ ran (,) ∧ 𝑓 ∈ ran (,) ) ∧ ( 𝑋 ∈ ( ℝ × ℝ ) ∧ 𝐴 = ( 𝑒 × 𝑓 ) ∧ 𝑋 ∈ ( 𝑒 × 𝑓 ) ) ) → ( 1st ‘ 𝑋 ) ∈ 𝑒 )
31 1 2 dya2icoseg2 ⊢ ( ( ( 1st ‘ 𝑋 ) ∈ ℝ ∧ 𝑒 ∈ ran (,) ∧ ( 1st ‘ 𝑋 ) ∈ 𝑒 ) → ∃ 𝑠 ∈ ran 𝐼 ( ( 1st ‘ 𝑋 ) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑒 ) )
32 26 27 30 31 syl3anc ⊢ ( ( ( 𝑒 ∈ ran (,) ∧ 𝑓 ∈ ran (,) ) ∧ ( 𝑋 ∈ ( ℝ × ℝ ) ∧ 𝐴 = ( 𝑒 × 𝑓 ) ∧ 𝑋 ∈ ( 𝑒 × 𝑓 ) ) ) → ∃ 𝑠 ∈ ran 𝐼 ( ( 1st ‘ 𝑋 ) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑒 ) )
33 xp2nd ⊢ ( 𝑋 ∈ ( ℝ × ℝ ) → ( 2nd ‘ 𝑋 ) ∈ ℝ )
34 33 3ad2ant1 ⊢ ( ( 𝑋 ∈ ( ℝ × ℝ ) ∧ 𝐴 = ( 𝑒 × 𝑓 ) ∧ 𝑋 ∈ ( 𝑒 × 𝑓 ) ) → ( 2nd ‘ 𝑋 ) ∈ ℝ )
35 34 adantl ⊢ ( ( ( 𝑒 ∈ ran (,) ∧ 𝑓 ∈ ran (,) ) ∧ ( 𝑋 ∈ ( ℝ × ℝ ) ∧ 𝐴 = ( 𝑒 × 𝑓 ) ∧ 𝑋 ∈ ( 𝑒 × 𝑓 ) ) ) → ( 2nd ‘ 𝑋 ) ∈ ℝ )
36 simplr ⊢ ( ( ( 𝑒 ∈ ran (,) ∧ 𝑓 ∈ ran (,) ) ∧ ( 𝑋 ∈ ( ℝ × ℝ ) ∧ 𝐴 = ( 𝑒 × 𝑓 ) ∧ 𝑋 ∈ ( 𝑒 × 𝑓 ) ) ) → 𝑓 ∈ ran (,) )
37 xp2nd ⊢ ( 𝑋 ∈ ( 𝑒 × 𝑓 ) → ( 2nd ‘ 𝑋 ) ∈ 𝑓 )
38 37 3ad2ant3 ⊢ ( ( 𝑋 ∈ ( ℝ × ℝ ) ∧ 𝐴 = ( 𝑒 × 𝑓 ) ∧ 𝑋 ∈ ( 𝑒 × 𝑓 ) ) → ( 2nd ‘ 𝑋 ) ∈ 𝑓 )
39 38 adantl ⊢ ( ( ( 𝑒 ∈ ran (,) ∧ 𝑓 ∈ ran (,) ) ∧ ( 𝑋 ∈ ( ℝ × ℝ ) ∧ 𝐴 = ( 𝑒 × 𝑓 ) ∧ 𝑋 ∈ ( 𝑒 × 𝑓 ) ) ) → ( 2nd ‘ 𝑋 ) ∈ 𝑓 )
40 1 2 dya2icoseg2 ⊢ ( ( ( 2nd ‘ 𝑋 ) ∈ ℝ ∧ 𝑓 ∈ ran (,) ∧ ( 2nd ‘ 𝑋 ) ∈ 𝑓 ) → ∃ 𝑡 ∈ ran 𝐼 ( ( 2nd ‘ 𝑋 ) ∈ 𝑡 ∧ 𝑡 ⊆ 𝑓 ) )
41 35 36 39 40 syl3anc ⊢ ( ( ( 𝑒 ∈ ran (,) ∧ 𝑓 ∈ ran (,) ) ∧ ( 𝑋 ∈ ( ℝ × ℝ ) ∧ 𝐴 = ( 𝑒 × 𝑓 ) ∧ 𝑋 ∈ ( 𝑒 × 𝑓 ) ) ) → ∃ 𝑡 ∈ ran 𝐼 ( ( 2nd ‘ 𝑋 ) ∈ 𝑡 ∧ 𝑡 ⊆ 𝑓 ) )
42 reeanv ⊢ ( ∃ 𝑠 ∈ ran 𝐼 ∃ 𝑡 ∈ ran 𝐼 ( ( ( 1st ‘ 𝑋 ) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑒 ) ∧ ( ( 2nd ‘ 𝑋 ) ∈ 𝑡 ∧ 𝑡 ⊆ 𝑓 ) ) ↔ ( ∃ 𝑠 ∈ ran 𝐼 ( ( 1st ‘ 𝑋 ) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑒 ) ∧ ∃ 𝑡 ∈ ran 𝐼 ( ( 2nd ‘ 𝑋 ) ∈ 𝑡 ∧ 𝑡 ⊆ 𝑓 ) ) )
43 32 41 42 sylanbrc ⊢ ( ( ( 𝑒 ∈ ran (,) ∧ 𝑓 ∈ ran (,) ) ∧ ( 𝑋 ∈ ( ℝ × ℝ ) ∧ 𝐴 = ( 𝑒 × 𝑓 ) ∧ 𝑋 ∈ ( 𝑒 × 𝑓 ) ) ) → ∃ 𝑠 ∈ ran 𝐼 ∃ 𝑡 ∈ ran 𝐼 ( ( ( 1st ‘ 𝑋 ) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑒 ) ∧ ( ( 2nd ‘ 𝑋 ) ∈ 𝑡 ∧ 𝑡 ⊆ 𝑓 ) ) )
44 eqid ⊢ ( 𝑠 × 𝑡 ) = ( 𝑠 × 𝑡 )
45 xpeq1 ⊢ ( 𝑢 = 𝑠 → ( 𝑢 × 𝑣 ) = ( 𝑠 × 𝑣 ) )
46 45 eqeq2d ⊢ ( 𝑢 = 𝑠 → ( ( 𝑠 × 𝑡 ) = ( 𝑢 × 𝑣 ) ↔ ( 𝑠 × 𝑡 ) = ( 𝑠 × 𝑣 ) ) )
47 xpeq2 ⊢ ( 𝑣 = 𝑡 → ( 𝑠 × 𝑣 ) = ( 𝑠 × 𝑡 ) )
48 47 eqeq2d ⊢ ( 𝑣 = 𝑡 → ( ( 𝑠 × 𝑡 ) = ( 𝑠 × 𝑣 ) ↔ ( 𝑠 × 𝑡 ) = ( 𝑠 × 𝑡 ) ) )
49 46 48 rspc2ev ⊢ ( ( 𝑠 ∈ ran 𝐼 ∧ 𝑡 ∈ ran 𝐼 ∧ ( 𝑠 × 𝑡 ) = ( 𝑠 × 𝑡 ) ) → ∃ 𝑢 ∈ ran 𝐼 ∃ 𝑣 ∈ ran 𝐼 ( 𝑠 × 𝑡 ) = ( 𝑢 × 𝑣 ) )
50 44 49 mp3an3 ⊢ ( ( 𝑠 ∈ ran 𝐼 ∧ 𝑡 ∈ ran 𝐼 ) → ∃ 𝑢 ∈ ran 𝐼 ∃ 𝑣 ∈ ran 𝐼 ( 𝑠 × 𝑡 ) = ( 𝑢 × 𝑣 ) )
51 vex ⊢ 𝑢 ∈ V
52 vex ⊢ 𝑣 ∈ V
53 51 52 xpex ⊢ ( 𝑢 × 𝑣 ) ∈ V
54 3 53 elrnmpo ⊢ ( ( 𝑠 × 𝑡 ) ∈ ran 𝑅 ↔ ∃ 𝑢 ∈ ran 𝐼 ∃ 𝑣 ∈ ran 𝐼 ( 𝑠 × 𝑡 ) = ( 𝑢 × 𝑣 ) )
55 50 54 sylibr ⊢ ( ( 𝑠 ∈ ran 𝐼 ∧ 𝑡 ∈ ran 𝐼 ) → ( 𝑠 × 𝑡 ) ∈ ran 𝑅 )
56 55 ad2antrl ⊢ ( ( ( 𝑋 ∈ ( ℝ × ℝ ) ∧ 𝐴 = ( 𝑒 × 𝑓 ) ∧ 𝑋 ∈ ( 𝑒 × 𝑓 ) ) ∧ ( ( 𝑠 ∈ ran 𝐼 ∧ 𝑡 ∈ ran 𝐼 ) ∧ ( ( ( 1st ‘ 𝑋 ) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑒 ) ∧ ( ( 2nd ‘ 𝑋 ) ∈ 𝑡 ∧ 𝑡 ⊆ 𝑓 ) ) ) ) → ( 𝑠 × 𝑡 ) ∈ ran 𝑅 )
57 xpss ⊢ ( ℝ × ℝ ) ⊆ ( V × V )
58 simpl1 ⊢ ( ( ( 𝑋 ∈ ( ℝ × ℝ ) ∧ 𝐴 = ( 𝑒 × 𝑓 ) ∧ 𝑋 ∈ ( 𝑒 × 𝑓 ) ) ∧ ( ( 𝑠 ∈ ran 𝐼 ∧ 𝑡 ∈ ran 𝐼 ) ∧ ( ( ( 1st ‘ 𝑋 ) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑒 ) ∧ ( ( 2nd ‘ 𝑋 ) ∈ 𝑡 ∧ 𝑡 ⊆ 𝑓 ) ) ) ) → 𝑋 ∈ ( ℝ × ℝ ) )
59 57 58 sseldi ⊢ ( ( ( 𝑋 ∈ ( ℝ × ℝ ) ∧ 𝐴 = ( 𝑒 × 𝑓 ) ∧ 𝑋 ∈ ( 𝑒 × 𝑓 ) ) ∧ ( ( 𝑠 ∈ ran 𝐼 ∧ 𝑡 ∈ ran 𝐼 ) ∧ ( ( ( 1st ‘ 𝑋 ) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑒 ) ∧ ( ( 2nd ‘ 𝑋 ) ∈ 𝑡 ∧ 𝑡 ⊆ 𝑓 ) ) ) ) → 𝑋 ∈ ( V × V ) )
60 simprrl ⊢ ( ( ( 𝑋 ∈ ( ℝ × ℝ ) ∧ 𝐴 = ( 𝑒 × 𝑓 ) ∧ 𝑋 ∈ ( 𝑒 × 𝑓 ) ) ∧ ( ( 𝑠 ∈ ran 𝐼 ∧ 𝑡 ∈ ran 𝐼 ) ∧ ( ( ( 1st ‘ 𝑋 ) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑒 ) ∧ ( ( 2nd ‘ 𝑋 ) ∈ 𝑡 ∧ 𝑡 ⊆ 𝑓 ) ) ) ) → ( ( 1st ‘ 𝑋 ) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑒 ) )
61 60 simpld ⊢ ( ( ( 𝑋 ∈ ( ℝ × ℝ ) ∧ 𝐴 = ( 𝑒 × 𝑓 ) ∧ 𝑋 ∈ ( 𝑒 × 𝑓 ) ) ∧ ( ( 𝑠 ∈ ran 𝐼 ∧ 𝑡 ∈ ran 𝐼 ) ∧ ( ( ( 1st ‘ 𝑋 ) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑒 ) ∧ ( ( 2nd ‘ 𝑋 ) ∈ 𝑡 ∧ 𝑡 ⊆ 𝑓 ) ) ) ) → ( 1st ‘ 𝑋 ) ∈ 𝑠 )
62 simprrr ⊢ ( ( ( 𝑋 ∈ ( ℝ × ℝ ) ∧ 𝐴 = ( 𝑒 × 𝑓 ) ∧ 𝑋 ∈ ( 𝑒 × 𝑓 ) ) ∧ ( ( 𝑠 ∈ ran 𝐼 ∧ 𝑡 ∈ ran 𝐼 ) ∧ ( ( ( 1st ‘ 𝑋 ) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑒 ) ∧ ( ( 2nd ‘ 𝑋 ) ∈ 𝑡 ∧ 𝑡 ⊆ 𝑓 ) ) ) ) → ( ( 2nd ‘ 𝑋 ) ∈ 𝑡 ∧ 𝑡 ⊆ 𝑓 ) )
63 62 simpld ⊢ ( ( ( 𝑋 ∈ ( ℝ × ℝ ) ∧ 𝐴 = ( 𝑒 × 𝑓 ) ∧ 𝑋 ∈ ( 𝑒 × 𝑓 ) ) ∧ ( ( 𝑠 ∈ ran 𝐼 ∧ 𝑡 ∈ ran 𝐼 ) ∧ ( ( ( 1st ‘ 𝑋 ) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑒 ) ∧ ( ( 2nd ‘ 𝑋 ) ∈ 𝑡 ∧ 𝑡 ⊆ 𝑓 ) ) ) ) → ( 2nd ‘ 𝑋 ) ∈ 𝑡 )
64 elxp7 ⊢ ( 𝑋 ∈ ( 𝑠 × 𝑡 ) ↔ ( 𝑋 ∈ ( V × V ) ∧ ( ( 1st ‘ 𝑋 ) ∈ 𝑠 ∧ ( 2nd ‘ 𝑋 ) ∈ 𝑡 ) ) )
65 64 biimpri ⊢ ( ( 𝑋 ∈ ( V × V ) ∧ ( ( 1st ‘ 𝑋 ) ∈ 𝑠 ∧ ( 2nd ‘ 𝑋 ) ∈ 𝑡 ) ) → 𝑋 ∈ ( 𝑠 × 𝑡 ) )
66 59 61 63 65 syl12anc ⊢ ( ( ( 𝑋 ∈ ( ℝ × ℝ ) ∧ 𝐴 = ( 𝑒 × 𝑓 ) ∧ 𝑋 ∈ ( 𝑒 × 𝑓 ) ) ∧ ( ( 𝑠 ∈ ran 𝐼 ∧ 𝑡 ∈ ran 𝐼 ) ∧ ( ( ( 1st ‘ 𝑋 ) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑒 ) ∧ ( ( 2nd ‘ 𝑋 ) ∈ 𝑡 ∧ 𝑡 ⊆ 𝑓 ) ) ) ) → 𝑋 ∈ ( 𝑠 × 𝑡 ) )
67 60 simprd ⊢ ( ( ( 𝑋 ∈ ( ℝ × ℝ ) ∧ 𝐴 = ( 𝑒 × 𝑓 ) ∧ 𝑋 ∈ ( 𝑒 × 𝑓 ) ) ∧ ( ( 𝑠 ∈ ran 𝐼 ∧ 𝑡 ∈ ran 𝐼 ) ∧ ( ( ( 1st ‘ 𝑋 ) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑒 ) ∧ ( ( 2nd ‘ 𝑋 ) ∈ 𝑡 ∧ 𝑡 ⊆ 𝑓 ) ) ) ) → 𝑠 ⊆ 𝑒 )
68 62 simprd ⊢ ( ( ( 𝑋 ∈ ( ℝ × ℝ ) ∧ 𝐴 = ( 𝑒 × 𝑓 ) ∧ 𝑋 ∈ ( 𝑒 × 𝑓 ) ) ∧ ( ( 𝑠 ∈ ran 𝐼 ∧ 𝑡 ∈ ran 𝐼 ) ∧ ( ( ( 1st ‘ 𝑋 ) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑒 ) ∧ ( ( 2nd ‘ 𝑋 ) ∈ 𝑡 ∧ 𝑡 ⊆ 𝑓 ) ) ) ) → 𝑡 ⊆ 𝑓 )
69 xpss12 ⊢ ( ( 𝑠 ⊆ 𝑒 ∧ 𝑡 ⊆ 𝑓 ) → ( 𝑠 × 𝑡 ) ⊆ ( 𝑒 × 𝑓 ) )
70 67 68 69 syl2anc ⊢ ( ( ( 𝑋 ∈ ( ℝ × ℝ ) ∧ 𝐴 = ( 𝑒 × 𝑓 ) ∧ 𝑋 ∈ ( 𝑒 × 𝑓 ) ) ∧ ( ( 𝑠 ∈ ran 𝐼 ∧ 𝑡 ∈ ran 𝐼 ) ∧ ( ( ( 1st ‘ 𝑋 ) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑒 ) ∧ ( ( 2nd ‘ 𝑋 ) ∈ 𝑡 ∧ 𝑡 ⊆ 𝑓 ) ) ) ) → ( 𝑠 × 𝑡 ) ⊆ ( 𝑒 × 𝑓 ) )
71 simpl2 ⊢ ( ( ( 𝑋 ∈ ( ℝ × ℝ ) ∧ 𝐴 = ( 𝑒 × 𝑓 ) ∧ 𝑋 ∈ ( 𝑒 × 𝑓 ) ) ∧ ( ( 𝑠 ∈ ran 𝐼 ∧ 𝑡 ∈ ran 𝐼 ) ∧ ( ( ( 1st ‘ 𝑋 ) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑒 ) ∧ ( ( 2nd ‘ 𝑋 ) ∈ 𝑡 ∧ 𝑡 ⊆ 𝑓 ) ) ) ) → 𝐴 = ( 𝑒 × 𝑓 ) )
72 70 71 sseqtrrd ⊢ ( ( ( 𝑋 ∈ ( ℝ × ℝ ) ∧ 𝐴 = ( 𝑒 × 𝑓 ) ∧ 𝑋 ∈ ( 𝑒 × 𝑓 ) ) ∧ ( ( 𝑠 ∈ ran 𝐼 ∧ 𝑡 ∈ ran 𝐼 ) ∧ ( ( ( 1st ‘ 𝑋 ) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑒 ) ∧ ( ( 2nd ‘ 𝑋 ) ∈ 𝑡 ∧ 𝑡 ⊆ 𝑓 ) ) ) ) → ( 𝑠 × 𝑡 ) ⊆ 𝐴 )
73 eleq2 ⊢ ( 𝑏 = ( 𝑠 × 𝑡 ) → ( 𝑋 ∈ 𝑏 ↔ 𝑋 ∈ ( 𝑠 × 𝑡 ) ) )
74 sseq1 ⊢ ( 𝑏 = ( 𝑠 × 𝑡 ) → ( 𝑏 ⊆ 𝐴 ↔ ( 𝑠 × 𝑡 ) ⊆ 𝐴 ) )
75 73 74 anbi12d ⊢ ( 𝑏 = ( 𝑠 × 𝑡 ) → ( ( 𝑋 ∈ 𝑏 ∧ 𝑏 ⊆ 𝐴 ) ↔ ( 𝑋 ∈ ( 𝑠 × 𝑡 ) ∧ ( 𝑠 × 𝑡 ) ⊆ 𝐴 ) ) )
76 75 rspcev ⊢ ( ( ( 𝑠 × 𝑡 ) ∈ ran 𝑅 ∧ ( 𝑋 ∈ ( 𝑠 × 𝑡 ) ∧ ( 𝑠 × 𝑡 ) ⊆ 𝐴 ) ) → ∃ 𝑏 ∈ ran 𝑅 ( 𝑋 ∈ 𝑏 ∧ 𝑏 ⊆ 𝐴 ) )
77 56 66 72 76 syl12anc ⊢ ( ( ( 𝑋 ∈ ( ℝ × ℝ ) ∧ 𝐴 = ( 𝑒 × 𝑓 ) ∧ 𝑋 ∈ ( 𝑒 × 𝑓 ) ) ∧ ( ( 𝑠 ∈ ran 𝐼 ∧ 𝑡 ∈ ran 𝐼 ) ∧ ( ( ( 1st ‘ 𝑋 ) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑒 ) ∧ ( ( 2nd ‘ 𝑋 ) ∈ 𝑡 ∧ 𝑡 ⊆ 𝑓 ) ) ) ) → ∃ 𝑏 ∈ ran 𝑅 ( 𝑋 ∈ 𝑏 ∧ 𝑏 ⊆ 𝐴 ) )
78 77 exp32 ⊢ ( ( 𝑋 ∈ ( ℝ × ℝ ) ∧ 𝐴 = ( 𝑒 × 𝑓 ) ∧ 𝑋 ∈ ( 𝑒 × 𝑓 ) ) → ( ( 𝑠 ∈ ran 𝐼 ∧ 𝑡 ∈ ran 𝐼 ) → ( ( ( ( 1st ‘ 𝑋 ) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑒 ) ∧ ( ( 2nd ‘ 𝑋 ) ∈ 𝑡 ∧ 𝑡 ⊆ 𝑓 ) ) → ∃ 𝑏 ∈ ran 𝑅 ( 𝑋 ∈ 𝑏 ∧ 𝑏 ⊆ 𝐴 ) ) ) )
79 78 rexlimdvv ⊢ ( ( 𝑋 ∈ ( ℝ × ℝ ) ∧ 𝐴 = ( 𝑒 × 𝑓 ) ∧ 𝑋 ∈ ( 𝑒 × 𝑓 ) ) → ( ∃ 𝑠 ∈ ran 𝐼 ∃ 𝑡 ∈ ran 𝐼 ( ( ( 1st ‘ 𝑋 ) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑒 ) ∧ ( ( 2nd ‘ 𝑋 ) ∈ 𝑡 ∧ 𝑡 ⊆ 𝑓 ) ) → ∃ 𝑏 ∈ ran 𝑅 ( 𝑋 ∈ 𝑏 ∧ 𝑏 ⊆ 𝐴 ) ) )
80 23 43 79 sylc ⊢ ( ( ( 𝑒 ∈ ran (,) ∧ 𝑓 ∈ ran (,) ) ∧ ( 𝑋 ∈ ( ℝ × ℝ ) ∧ 𝐴 = ( 𝑒 × 𝑓 ) ∧ 𝑋 ∈ ( 𝑒 × 𝑓 ) ) ) → ∃ 𝑏 ∈ ran 𝑅 ( 𝑋 ∈ 𝑏 ∧ 𝑏 ⊆ 𝐴 ) )
81 22 80 sylan2 ⊢ ( ( ( 𝑒 ∈ ran (,) ∧ 𝑓 ∈ ran (,) ) ∧ ( 𝐴 = ( 𝑒 × 𝑓 ) ∧ ( 𝑋 ∈ ( ℝ × ℝ ) ∧ 𝑋 ∈ 𝐴 ) ) ) → ∃ 𝑏 ∈ ran 𝑅 ( 𝑋 ∈ 𝑏 ∧ 𝑏 ⊆ 𝐴 ) )
82 81 ex ⊢ ( ( 𝑒 ∈ ran (,) ∧ 𝑓 ∈ ran (,) ) → ( ( 𝐴 = ( 𝑒 × 𝑓 ) ∧ ( 𝑋 ∈ ( ℝ × ℝ ) ∧ 𝑋 ∈ 𝐴 ) ) → ∃ 𝑏 ∈ ran 𝑅 ( 𝑋 ∈ 𝑏 ∧ 𝑏 ⊆ 𝐴 ) ) )
83 82 rexlimivv ⊢ ( ∃ 𝑒 ∈ ran (,) ∃ 𝑓 ∈ ran (,) ( 𝐴 = ( 𝑒 × 𝑓 ) ∧ ( 𝑋 ∈ ( ℝ × ℝ ) ∧ 𝑋 ∈ 𝐴 ) ) → ∃ 𝑏 ∈ ran 𝑅 ( 𝑋 ∈ 𝑏 ∧ 𝑏 ⊆ 𝐴 ) )
84 15 17 83 3syl ⊢ ( ( 𝑋 ∈ ( ℝ × ℝ ) ∧ 𝐴 ∈ 𝐵 ∧ 𝑋 ∈ 𝐴 ) → ∃ 𝑏 ∈ ran 𝑅 ( 𝑋 ∈ 𝑏 ∧ 𝑏 ⊆ 𝐴 ) )