Metamath Proof Explorer

Theorem bndth

Description: The Boundedness Theorem. A continuous function from a compact topological space to the reals is bounded (above). (Boundedness below is obtained by applying this theorem to -u F .) (Contributed by Mario Carneiro, 12-Aug-2014)

Ref Expression
Hypotheses bndth.1 ⊢ 𝑋 = ∪ 𝐽
bndth.2 ⊢ 𝐾 = ( topGen ‘ ran (,) )
bndth.3 ⊢ ( 𝜑 → 𝐽 ∈ Comp )
bndth.4 ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
Assertion bndth ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝑋 ( 𝐹 ‘ 𝑦 ) ≤ 𝑥 )

Proof

Step Hyp Ref Expression
1 bndth.1 ⊢ 𝑋 = ∪ 𝐽
2 bndth.2 ⊢ 𝐾 = ( topGen ‘ ran (,) )
3 bndth.3 ⊢ ( 𝜑 → 𝐽 ∈ Comp )
4 bndth.4 ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
5 retopon ⊢ ( topGen ‘ ran (,) ) ∈ ( TopOn ‘ ℝ )
6 2 5 eqeltri ⊢ 𝐾 ∈ ( TopOn ‘ ℝ )
7 6 toponunii ⊢ ℝ = ∪ 𝐾
8 1 7 cnf ⊢ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐹 : 𝑋 ⟶ ℝ )
9 4 8 syl ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ℝ )
10 9 frnd ⊢ ( 𝜑 → ran 𝐹 ⊆ ℝ )
11 unieq ⊢ ( 𝑢 = ( (,) “ ( { -∞ } × ℝ ) ) → ∪ 𝑢 = ∪ ( (,) “ ( { -∞ } × ℝ ) ) )
12 imassrn ⊢ ( (,) “ ( { -∞ } × ℝ ) ) ⊆ ran (,)
13 12 unissi ⊢ ∪ ( (,) “ ( { -∞ } × ℝ ) ) ⊆ ∪ ran (,)
14 unirnioo ⊢ ℝ = ∪ ran (,)
15 13 14 sseqtrri ⊢ ∪ ( (,) “ ( { -∞ } × ℝ ) ) ⊆ ℝ
16 id ⊢ ( 𝑥 ∈ ℝ → 𝑥 ∈ ℝ )
17 ltp1 ⊢ ( 𝑥 ∈ ℝ → 𝑥 < ( 𝑥 + 1 ) )
18 ressxr ⊢ ℝ ⊆ ℝ*
19 peano2re ⊢ ( 𝑥 ∈ ℝ → ( 𝑥 + 1 ) ∈ ℝ )
20 18 19 sselid ⊢ ( 𝑥 ∈ ℝ → ( 𝑥 + 1 ) ∈ ℝ* )
21 elioomnf ⊢ ( ( 𝑥 + 1 ) ∈ ℝ* → ( 𝑥 ∈ ( -∞ (,) ( 𝑥 + 1 ) ) ↔ ( 𝑥 ∈ ℝ ∧ 𝑥 < ( 𝑥 + 1 ) ) ) )
22 20 21 syl ⊢ ( 𝑥 ∈ ℝ → ( 𝑥 ∈ ( -∞ (,) ( 𝑥 + 1 ) ) ↔ ( 𝑥 ∈ ℝ ∧ 𝑥 < ( 𝑥 + 1 ) ) ) )
23 16 17 22 mpbir2and ⊢ ( 𝑥 ∈ ℝ → 𝑥 ∈ ( -∞ (,) ( 𝑥 + 1 ) ) )
24 df-ov ⊢ ( -∞ (,) ( 𝑥 + 1 ) ) = ( (,) ‘ ⟨ -∞ , ( 𝑥 + 1 ) ⟩ )
25 mnfxr ⊢ -∞ ∈ ℝ*
26 25 elexi ⊢ -∞ ∈ V
27 26 snid ⊢ -∞ ∈ { -∞ }
28 opelxpi ⊢ ( ( -∞ ∈ { -∞ } ∧ ( 𝑥 + 1 ) ∈ ℝ ) → ⟨ -∞ , ( 𝑥 + 1 ) ⟩ ∈ ( { -∞ } × ℝ ) )
29 27 19 28 sylancr ⊢ ( 𝑥 ∈ ℝ → ⟨ -∞ , ( 𝑥 + 1 ) ⟩ ∈ ( { -∞ } × ℝ ) )
30 ioof ⊢ (,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ
31 ffun ⊢ ( (,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ → Fun (,) )
32 30 31 ax-mp ⊢ Fun (,)
33 snssi ⊢ ( -∞ ∈ ℝ* → { -∞ } ⊆ ℝ* )
34 25 33 ax-mp ⊢ { -∞ } ⊆ ℝ*
35 xpss12 ⊢ ( ( { -∞ } ⊆ ℝ* ∧ ℝ ⊆ ℝ* ) → ( { -∞ } × ℝ ) ⊆ ( ℝ* × ℝ* ) )
36 34 18 35 mp2an ⊢ ( { -∞ } × ℝ ) ⊆ ( ℝ* × ℝ* )
37 30 fdmi ⊢ dom (,) = ( ℝ* × ℝ* )
38 36 37 sseqtrri ⊢ ( { -∞ } × ℝ ) ⊆ dom (,)
39 funfvima2 ⊢ ( ( Fun (,) ∧ ( { -∞ } × ℝ ) ⊆ dom (,) ) → ( ⟨ -∞ , ( 𝑥 + 1 ) ⟩ ∈ ( { -∞ } × ℝ ) → ( (,) ‘ ⟨ -∞ , ( 𝑥 + 1 ) ⟩ ) ∈ ( (,) “ ( { -∞ } × ℝ ) ) ) )
40 32 38 39 mp2an ⊢ ( ⟨ -∞ , ( 𝑥 + 1 ) ⟩ ∈ ( { -∞ } × ℝ ) → ( (,) ‘ ⟨ -∞ , ( 𝑥 + 1 ) ⟩ ) ∈ ( (,) “ ( { -∞ } × ℝ ) ) )
41 29 40 syl ⊢ ( 𝑥 ∈ ℝ → ( (,) ‘ ⟨ -∞ , ( 𝑥 + 1 ) ⟩ ) ∈ ( (,) “ ( { -∞ } × ℝ ) ) )
42 24 41 eqeltrid ⊢ ( 𝑥 ∈ ℝ → ( -∞ (,) ( 𝑥 + 1 ) ) ∈ ( (,) “ ( { -∞ } × ℝ ) ) )
43 elunii ⊢ ( ( 𝑥 ∈ ( -∞ (,) ( 𝑥 + 1 ) ) ∧ ( -∞ (,) ( 𝑥 + 1 ) ) ∈ ( (,) “ ( { -∞ } × ℝ ) ) ) → 𝑥 ∈ ∪ ( (,) “ ( { -∞ } × ℝ ) ) )
44 23 42 43 syl2anc ⊢ ( 𝑥 ∈ ℝ → 𝑥 ∈ ∪ ( (,) “ ( { -∞ } × ℝ ) ) )
45 44 ssriv ⊢ ℝ ⊆ ∪ ( (,) “ ( { -∞ } × ℝ ) )
46 15 45 eqssi ⊢ ∪ ( (,) “ ( { -∞ } × ℝ ) ) = ℝ
47 11 46 eqtrdi ⊢ ( 𝑢 = ( (,) “ ( { -∞ } × ℝ ) ) → ∪ 𝑢 = ℝ )
48 47 sseq2d ⊢ ( 𝑢 = ( (,) “ ( { -∞ } × ℝ ) ) → ( ran 𝐹 ⊆ ∪ 𝑢 ↔ ran 𝐹 ⊆ ℝ ) )
49 pweq ⊢ ( 𝑢 = ( (,) “ ( { -∞ } × ℝ ) ) → 𝒫 𝑢 = 𝒫 ( (,) “ ( { -∞ } × ℝ ) ) )
50 49 ineq1d ⊢ ( 𝑢 = ( (,) “ ( { -∞ } × ℝ ) ) → ( 𝒫 𝑢 ∩ Fin ) = ( 𝒫 ( (,) “ ( { -∞ } × ℝ ) ) ∩ Fin ) )
51 50 rexeqdv ⊢ ( 𝑢 = ( (,) “ ( { -∞ } × ℝ ) ) → ( ∃ 𝑣 ∈ ( 𝒫 𝑢 ∩ Fin ) ran 𝐹 ⊆ ∪ 𝑣 ↔ ∃ 𝑣 ∈ ( 𝒫 ( (,) “ ( { -∞ } × ℝ ) ) ∩ Fin ) ran 𝐹 ⊆ ∪ 𝑣 ) )
52 48 51 imbi12d ⊢ ( 𝑢 = ( (,) “ ( { -∞ } × ℝ ) ) → ( ( ran 𝐹 ⊆ ∪ 𝑢 → ∃ 𝑣 ∈ ( 𝒫 𝑢 ∩ Fin ) ran 𝐹 ⊆ ∪ 𝑣 ) ↔ ( ran 𝐹 ⊆ ℝ → ∃ 𝑣 ∈ ( 𝒫 ( (,) “ ( { -∞ } × ℝ ) ) ∩ Fin ) ran 𝐹 ⊆ ∪ 𝑣 ) ) )
53 rncmp ⊢ ( ( 𝐽 ∈ Comp ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → ( 𝐾 ↾t ran 𝐹 ) ∈ Comp )
54 3 4 53 syl2anc ⊢ ( 𝜑 → ( 𝐾 ↾t ran 𝐹 ) ∈ Comp )
55 retop ⊢ ( topGen ‘ ran (,) ) ∈ Top
56 2 55 eqeltri ⊢ 𝐾 ∈ Top
57 7 cmpsub ⊢ ( ( 𝐾 ∈ Top ∧ ran 𝐹 ⊆ ℝ ) → ( ( 𝐾 ↾t ran 𝐹 ) ∈ Comp ↔ ∀ 𝑢 ∈ 𝒫 𝐾 ( ran 𝐹 ⊆ ∪ 𝑢 → ∃ 𝑣 ∈ ( 𝒫 𝑢 ∩ Fin ) ran 𝐹 ⊆ ∪ 𝑣 ) ) )
58 56 10 57 sylancr ⊢ ( 𝜑 → ( ( 𝐾 ↾t ran 𝐹 ) ∈ Comp ↔ ∀ 𝑢 ∈ 𝒫 𝐾 ( ran 𝐹 ⊆ ∪ 𝑢 → ∃ 𝑣 ∈ ( 𝒫 𝑢 ∩ Fin ) ran 𝐹 ⊆ ∪ 𝑣 ) ) )
59 54 58 mpbid ⊢ ( 𝜑 → ∀ 𝑢 ∈ 𝒫 𝐾 ( ran 𝐹 ⊆ ∪ 𝑢 → ∃ 𝑣 ∈ ( 𝒫 𝑢 ∩ Fin ) ran 𝐹 ⊆ ∪ 𝑣 ) )
60 retopbas ⊢ ran (,) ∈ TopBases
61 bastg ⊢ ( ran (,) ∈ TopBases → ran (,) ⊆ ( topGen ‘ ran (,) ) )
62 60 61 ax-mp ⊢ ran (,) ⊆ ( topGen ‘ ran (,) )
63 62 2 sseqtrri ⊢ ran (,) ⊆ 𝐾
64 12 63 sstri ⊢ ( (,) “ ( { -∞ } × ℝ ) ) ⊆ 𝐾
65 56 64 elpwi2 ⊢ ( (,) “ ( { -∞ } × ℝ ) ) ∈ 𝒫 𝐾
66 65 a1i ⊢ ( 𝜑 → ( (,) “ ( { -∞ } × ℝ ) ) ∈ 𝒫 𝐾 )
67 52 59 66 rspcdva ⊢ ( 𝜑 → ( ran 𝐹 ⊆ ℝ → ∃ 𝑣 ∈ ( 𝒫 ( (,) “ ( { -∞ } × ℝ ) ) ∩ Fin ) ran 𝐹 ⊆ ∪ 𝑣 ) )
68 10 67 mpd ⊢ ( 𝜑 → ∃ 𝑣 ∈ ( 𝒫 ( (,) “ ( { -∞ } × ℝ ) ) ∩ Fin ) ran 𝐹 ⊆ ∪ 𝑣 )
69 simpr ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 𝒫 ( (,) “ ( { -∞ } × ℝ ) ) ∩ Fin ) ) → 𝑣 ∈ ( 𝒫 ( (,) “ ( { -∞ } × ℝ ) ) ∩ Fin ) )
70 elin ⊢ ( 𝑣 ∈ ( 𝒫 ( (,) “ ( { -∞ } × ℝ ) ) ∩ Fin ) ↔ ( 𝑣 ∈ 𝒫 ( (,) “ ( { -∞ } × ℝ ) ) ∧ 𝑣 ∈ Fin ) )
71 69 70 sylib ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 𝒫 ( (,) “ ( { -∞ } × ℝ ) ) ∩ Fin ) ) → ( 𝑣 ∈ 𝒫 ( (,) “ ( { -∞ } × ℝ ) ) ∧ 𝑣 ∈ Fin ) )
72 71 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( 𝒫 ( (,) “ ( { -∞ } × ℝ ) ) ∩ Fin ) ∧ ran 𝐹 ⊆ ∪ 𝑣 ) ) → ( 𝑣 ∈ 𝒫 ( (,) “ ( { -∞ } × ℝ ) ) ∧ 𝑣 ∈ Fin ) )
73 72 simprd ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( 𝒫 ( (,) “ ( { -∞ } × ℝ ) ) ∩ Fin ) ∧ ran 𝐹 ⊆ ∪ 𝑣 ) ) → 𝑣 ∈ Fin )
74 71 simpld ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 𝒫 ( (,) “ ( { -∞ } × ℝ ) ) ∩ Fin ) ) → 𝑣 ∈ 𝒫 ( (,) “ ( { -∞ } × ℝ ) ) )
75 74 elpwid ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 𝒫 ( (,) “ ( { -∞ } × ℝ ) ) ∩ Fin ) ) → 𝑣 ⊆ ( (,) “ ( { -∞ } × ℝ ) ) )
76 34 sseli ⊢ ( 𝑢 ∈ { -∞ } → 𝑢 ∈ ℝ* )
77 76 adantr ⊢ ( ( 𝑢 ∈ { -∞ } ∧ 𝑤 ∈ ℝ ) → 𝑢 ∈ ℝ* )
78 18 sseli ⊢ ( 𝑤 ∈ ℝ → 𝑤 ∈ ℝ* )
79 78 adantl ⊢ ( ( 𝑢 ∈ { -∞ } ∧ 𝑤 ∈ ℝ ) → 𝑤 ∈ ℝ* )
80 mnflt ⊢ ( 𝑤 ∈ ℝ → -∞ < 𝑤 )
81 xrltnle ⊢ ( ( -∞ ∈ ℝ* ∧ 𝑤 ∈ ℝ* ) → ( -∞ < 𝑤 ↔ ¬ 𝑤 ≤ -∞ ) )
82 25 78 81 sylancr ⊢ ( 𝑤 ∈ ℝ → ( -∞ < 𝑤 ↔ ¬ 𝑤 ≤ -∞ ) )
83 80 82 mpbid ⊢ ( 𝑤 ∈ ℝ → ¬ 𝑤 ≤ -∞ )
84 83 adantl ⊢ ( ( 𝑢 ∈ { -∞ } ∧ 𝑤 ∈ ℝ ) → ¬ 𝑤 ≤ -∞ )
85 elsni ⊢ ( 𝑢 ∈ { -∞ } → 𝑢 = -∞ )
86 85 adantr ⊢ ( ( 𝑢 ∈ { -∞ } ∧ 𝑤 ∈ ℝ ) → 𝑢 = -∞ )
87 86 breq2d ⊢ ( ( 𝑢 ∈ { -∞ } ∧ 𝑤 ∈ ℝ ) → ( 𝑤 ≤ 𝑢 ↔ 𝑤 ≤ -∞ ) )
88 84 87 mtbird ⊢ ( ( 𝑢 ∈ { -∞ } ∧ 𝑤 ∈ ℝ ) → ¬ 𝑤 ≤ 𝑢 )
89 ioo0 ⊢ ( ( 𝑢 ∈ ℝ* ∧ 𝑤 ∈ ℝ* ) → ( ( 𝑢 (,) 𝑤 ) = ∅ ↔ 𝑤 ≤ 𝑢 ) )
90 76 78 89 syl2an ⊢ ( ( 𝑢 ∈ { -∞ } ∧ 𝑤 ∈ ℝ ) → ( ( 𝑢 (,) 𝑤 ) = ∅ ↔ 𝑤 ≤ 𝑢 ) )
91 90 necon3abid ⊢ ( ( 𝑢 ∈ { -∞ } ∧ 𝑤 ∈ ℝ ) → ( ( 𝑢 (,) 𝑤 ) ≠ ∅ ↔ ¬ 𝑤 ≤ 𝑢 ) )
92 88 91 mpbird ⊢ ( ( 𝑢 ∈ { -∞ } ∧ 𝑤 ∈ ℝ ) → ( 𝑢 (,) 𝑤 ) ≠ ∅ )
93 df-ioo ⊢ (,) = ( 𝑦 ∈ ℝ* , 𝑧 ∈ ℝ* ↦ { 𝑣 ∈ ℝ* ∣ ( 𝑦 < 𝑣 ∧ 𝑣 < 𝑧 ) } )
94 idd ⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑤 ∈ ℝ* ) → ( 𝑥 < 𝑤 → 𝑥 < 𝑤 ) )
95 xrltle ⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑤 ∈ ℝ* ) → ( 𝑥 < 𝑤 → 𝑥 ≤ 𝑤 ) )
96 idd ⊢ ( ( 𝑢 ∈ ℝ* ∧ 𝑥 ∈ ℝ* ) → ( 𝑢 < 𝑥 → 𝑢 < 𝑥 ) )
97 xrltle ⊢ ( ( 𝑢 ∈ ℝ* ∧ 𝑥 ∈ ℝ* ) → ( 𝑢 < 𝑥 → 𝑢 ≤ 𝑥 ) )
98 93 94 95 96 97 ixxub ⊢ ( ( 𝑢 ∈ ℝ* ∧ 𝑤 ∈ ℝ* ∧ ( 𝑢 (,) 𝑤 ) ≠ ∅ ) → sup ( ( 𝑢 (,) 𝑤 ) , ℝ* , < ) = 𝑤 )
99 77 79 92 98 syl3anc ⊢ ( ( 𝑢 ∈ { -∞ } ∧ 𝑤 ∈ ℝ ) → sup ( ( 𝑢 (,) 𝑤 ) , ℝ* , < ) = 𝑤 )
100 simpr ⊢ ( ( 𝑢 ∈ { -∞ } ∧ 𝑤 ∈ ℝ ) → 𝑤 ∈ ℝ )
101 99 100 eqeltrd ⊢ ( ( 𝑢 ∈ { -∞ } ∧ 𝑤 ∈ ℝ ) → sup ( ( 𝑢 (,) 𝑤 ) , ℝ* , < ) ∈ ℝ )
102 101 rgen2 ⊢ ∀ 𝑢 ∈ { -∞ } ∀ 𝑤 ∈ ℝ sup ( ( 𝑢 (,) 𝑤 ) , ℝ* , < ) ∈ ℝ
103 fveq2 ⊢ ( 𝑧 = ⟨ 𝑢 , 𝑤 ⟩ → ( (,) ‘ 𝑧 ) = ( (,) ‘ ⟨ 𝑢 , 𝑤 ⟩ ) )
104 df-ov ⊢ ( 𝑢 (,) 𝑤 ) = ( (,) ‘ ⟨ 𝑢 , 𝑤 ⟩ )
105 103 104 eqtr4di ⊢ ( 𝑧 = ⟨ 𝑢 , 𝑤 ⟩ → ( (,) ‘ 𝑧 ) = ( 𝑢 (,) 𝑤 ) )
106 105 supeq1d ⊢ ( 𝑧 = ⟨ 𝑢 , 𝑤 ⟩ → sup ( ( (,) ‘ 𝑧 ) , ℝ* , < ) = sup ( ( 𝑢 (,) 𝑤 ) , ℝ* , < ) )
107 106 eleq1d ⊢ ( 𝑧 = ⟨ 𝑢 , 𝑤 ⟩ → ( sup ( ( (,) ‘ 𝑧 ) , ℝ* , < ) ∈ ℝ ↔ sup ( ( 𝑢 (,) 𝑤 ) , ℝ* , < ) ∈ ℝ ) )
108 107 ralxp ⊢ ( ∀ 𝑧 ∈ ( { -∞ } × ℝ ) sup ( ( (,) ‘ 𝑧 ) , ℝ* , < ) ∈ ℝ ↔ ∀ 𝑢 ∈ { -∞ } ∀ 𝑤 ∈ ℝ sup ( ( 𝑢 (,) 𝑤 ) , ℝ* , < ) ∈ ℝ )
109 102 108 mpbir ⊢ ∀ 𝑧 ∈ ( { -∞ } × ℝ ) sup ( ( (,) ‘ 𝑧 ) , ℝ* , < ) ∈ ℝ
110 ffn ⊢ ( (,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ → (,) Fn ( ℝ* × ℝ* ) )
111 30 110 ax-mp ⊢ (,) Fn ( ℝ* × ℝ* )
112 supeq1 ⊢ ( 𝑤 = ( (,) ‘ 𝑧 ) → sup ( 𝑤 , ℝ* , < ) = sup ( ( (,) ‘ 𝑧 ) , ℝ* , < ) )
113 112 eleq1d ⊢ ( 𝑤 = ( (,) ‘ 𝑧 ) → ( sup ( 𝑤 , ℝ* , < ) ∈ ℝ ↔ sup ( ( (,) ‘ 𝑧 ) , ℝ* , < ) ∈ ℝ ) )
114 113 ralima ⊢ ( ( (,) Fn ( ℝ* × ℝ* ) ∧ ( { -∞ } × ℝ ) ⊆ ( ℝ* × ℝ* ) ) → ( ∀ 𝑤 ∈ ( (,) “ ( { -∞ } × ℝ ) ) sup ( 𝑤 , ℝ* , < ) ∈ ℝ ↔ ∀ 𝑧 ∈ ( { -∞ } × ℝ ) sup ( ( (,) ‘ 𝑧 ) , ℝ* , < ) ∈ ℝ ) )
115 111 36 114 mp2an ⊢ ( ∀ 𝑤 ∈ ( (,) “ ( { -∞ } × ℝ ) ) sup ( 𝑤 , ℝ* , < ) ∈ ℝ ↔ ∀ 𝑧 ∈ ( { -∞ } × ℝ ) sup ( ( (,) ‘ 𝑧 ) , ℝ* , < ) ∈ ℝ )
116 109 115 mpbir ⊢ ∀ 𝑤 ∈ ( (,) “ ( { -∞ } × ℝ ) ) sup ( 𝑤 , ℝ* , < ) ∈ ℝ
117 ssralv ⊢ ( 𝑣 ⊆ ( (,) “ ( { -∞ } × ℝ ) ) → ( ∀ 𝑤 ∈ ( (,) “ ( { -∞ } × ℝ ) ) sup ( 𝑤 , ℝ* , < ) ∈ ℝ → ∀ 𝑤 ∈ 𝑣 sup ( 𝑤 , ℝ* , < ) ∈ ℝ ) )
118 75 116 117 mpisyl ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 𝒫 ( (,) “ ( { -∞ } × ℝ ) ) ∩ Fin ) ) → ∀ 𝑤 ∈ 𝑣 sup ( 𝑤 , ℝ* , < ) ∈ ℝ )
119 118 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( 𝒫 ( (,) “ ( { -∞ } × ℝ ) ) ∩ Fin ) ∧ ran 𝐹 ⊆ ∪ 𝑣 ) ) → ∀ 𝑤 ∈ 𝑣 sup ( 𝑤 , ℝ* , < ) ∈ ℝ )
120 fimaxre3 ⊢ ( ( 𝑣 ∈ Fin ∧ ∀ 𝑤 ∈ 𝑣 sup ( 𝑤 , ℝ* , < ) ∈ ℝ ) → ∃ 𝑥 ∈ ℝ ∀ 𝑤 ∈ 𝑣 sup ( 𝑤 , ℝ* , < ) ≤ 𝑥 )
121 73 119 120 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( 𝒫 ( (,) “ ( { -∞ } × ℝ ) ) ∩ Fin ) ∧ ran 𝐹 ⊆ ∪ 𝑣 ) ) → ∃ 𝑥 ∈ ℝ ∀ 𝑤 ∈ 𝑣 sup ( 𝑤 , ℝ* , < ) ≤ 𝑥 )
122 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ ( 𝒫 ( (,) “ ( { -∞ } × ℝ ) ) ∩ Fin ) ∧ ran 𝐹 ⊆ ∪ 𝑣 ) ) ∧ 𝑥 ∈ ℝ ) → ran 𝐹 ⊆ ∪ 𝑣 )
123 122 sselda ⊢ ( ( ( ( 𝜑 ∧ ( 𝑣 ∈ ( 𝒫 ( (,) “ ( { -∞ } × ℝ ) ) ∩ Fin ) ∧ ran 𝐹 ⊆ ∪ 𝑣 ) ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑧 ∈ ran 𝐹 ) → 𝑧 ∈ ∪ 𝑣 )
124 eluni2 ⊢ ( 𝑧 ∈ ∪ 𝑣 ↔ ∃ 𝑤 ∈ 𝑣 𝑧 ∈ 𝑤 )
125 r19.29r ⊢ ( ( ∃ 𝑤 ∈ 𝑣 𝑧 ∈ 𝑤 ∧ ∀ 𝑤 ∈ 𝑣 sup ( 𝑤 , ℝ* , < ) ≤ 𝑥 ) → ∃ 𝑤 ∈ 𝑣 ( 𝑧 ∈ 𝑤 ∧ sup ( 𝑤 , ℝ* , < ) ≤ 𝑥 ) )
126 sspwuni ⊢ ( ( (,) “ ( { -∞ } × ℝ ) ) ⊆ 𝒫 ℝ ↔ ∪ ( (,) “ ( { -∞ } × ℝ ) ) ⊆ ℝ )
127 15 126 mpbir ⊢ ( (,) “ ( { -∞ } × ℝ ) ) ⊆ 𝒫 ℝ
128 75 3ad2ant1 ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝒫 ( (,) “ ( { -∞ } × ℝ ) ) ∩ Fin ) ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑤 ∈ 𝑣 ) ∧ ( 𝑧 ∈ 𝑤 ∧ sup ( 𝑤 , ℝ* , < ) ≤ 𝑥 ) ) → 𝑣 ⊆ ( (,) “ ( { -∞ } × ℝ ) ) )
129 simp2r ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝒫 ( (,) “ ( { -∞ } × ℝ ) ) ∩ Fin ) ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑤 ∈ 𝑣 ) ∧ ( 𝑧 ∈ 𝑤 ∧ sup ( 𝑤 , ℝ* , < ) ≤ 𝑥 ) ) → 𝑤 ∈ 𝑣 )
130 128 129 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝒫 ( (,) “ ( { -∞ } × ℝ ) ) ∩ Fin ) ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑤 ∈ 𝑣 ) ∧ ( 𝑧 ∈ 𝑤 ∧ sup ( 𝑤 , ℝ* , < ) ≤ 𝑥 ) ) → 𝑤 ∈ ( (,) “ ( { -∞ } × ℝ ) ) )
131 127 130 sselid ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝒫 ( (,) “ ( { -∞ } × ℝ ) ) ∩ Fin ) ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑤 ∈ 𝑣 ) ∧ ( 𝑧 ∈ 𝑤 ∧ sup ( 𝑤 , ℝ* , < ) ≤ 𝑥 ) ) → 𝑤 ∈ 𝒫 ℝ )
132 131 elpwid ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝒫 ( (,) “ ( { -∞ } × ℝ ) ) ∩ Fin ) ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑤 ∈ 𝑣 ) ∧ ( 𝑧 ∈ 𝑤 ∧ sup ( 𝑤 , ℝ* , < ) ≤ 𝑥 ) ) → 𝑤 ⊆ ℝ )
133 simp3l ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝒫 ( (,) “ ( { -∞ } × ℝ ) ) ∩ Fin ) ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑤 ∈ 𝑣 ) ∧ ( 𝑧 ∈ 𝑤 ∧ sup ( 𝑤 , ℝ* , < ) ≤ 𝑥 ) ) → 𝑧 ∈ 𝑤 )
134 132 133 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝒫 ( (,) “ ( { -∞ } × ℝ ) ) ∩ Fin ) ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑤 ∈ 𝑣 ) ∧ ( 𝑧 ∈ 𝑤 ∧ sup ( 𝑤 , ℝ* , < ) ≤ 𝑥 ) ) → 𝑧 ∈ ℝ )
135 118 r19.21bi ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝒫 ( (,) “ ( { -∞ } × ℝ ) ) ∩ Fin ) ) ∧ 𝑤 ∈ 𝑣 ) → sup ( 𝑤 , ℝ* , < ) ∈ ℝ )
136 135 adantrl ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝒫 ( (,) “ ( { -∞ } × ℝ ) ) ∩ Fin ) ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑤 ∈ 𝑣 ) ) → sup ( 𝑤 , ℝ* , < ) ∈ ℝ )
137 136 3adant3 ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝒫 ( (,) “ ( { -∞ } × ℝ ) ) ∩ Fin ) ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑤 ∈ 𝑣 ) ∧ ( 𝑧 ∈ 𝑤 ∧ sup ( 𝑤 , ℝ* , < ) ≤ 𝑥 ) ) → sup ( 𝑤 , ℝ* , < ) ∈ ℝ )
138 simp2l ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝒫 ( (,) “ ( { -∞ } × ℝ ) ) ∩ Fin ) ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑤 ∈ 𝑣 ) ∧ ( 𝑧 ∈ 𝑤 ∧ sup ( 𝑤 , ℝ* , < ) ≤ 𝑥 ) ) → 𝑥 ∈ ℝ )
139 132 18 sstrdi ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝒫 ( (,) “ ( { -∞ } × ℝ ) ) ∩ Fin ) ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑤 ∈ 𝑣 ) ∧ ( 𝑧 ∈ 𝑤 ∧ sup ( 𝑤 , ℝ* , < ) ≤ 𝑥 ) ) → 𝑤 ⊆ ℝ* )
140 supxrub ⊢ ( ( 𝑤 ⊆ ℝ* ∧ 𝑧 ∈ 𝑤 ) → 𝑧 ≤ sup ( 𝑤 , ℝ* , < ) )
141 139 133 140 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝒫 ( (,) “ ( { -∞ } × ℝ ) ) ∩ Fin ) ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑤 ∈ 𝑣 ) ∧ ( 𝑧 ∈ 𝑤 ∧ sup ( 𝑤 , ℝ* , < ) ≤ 𝑥 ) ) → 𝑧 ≤ sup ( 𝑤 , ℝ* , < ) )
142 simp3r ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝒫 ( (,) “ ( { -∞ } × ℝ ) ) ∩ Fin ) ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑤 ∈ 𝑣 ) ∧ ( 𝑧 ∈ 𝑤 ∧ sup ( 𝑤 , ℝ* , < ) ≤ 𝑥 ) ) → sup ( 𝑤 , ℝ* , < ) ≤ 𝑥 )
143 134 137 138 141 142 letrd ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝒫 ( (,) “ ( { -∞ } × ℝ ) ) ∩ Fin ) ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑤 ∈ 𝑣 ) ∧ ( 𝑧 ∈ 𝑤 ∧ sup ( 𝑤 , ℝ* , < ) ≤ 𝑥 ) ) → 𝑧 ≤ 𝑥 )
144 143 3expia ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝒫 ( (,) “ ( { -∞ } × ℝ ) ) ∩ Fin ) ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑤 ∈ 𝑣 ) ) → ( ( 𝑧 ∈ 𝑤 ∧ sup ( 𝑤 , ℝ* , < ) ≤ 𝑥 ) → 𝑧 ≤ 𝑥 ) )
145 144 anassrs ⊢ ( ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝒫 ( (,) “ ( { -∞ } × ℝ ) ) ∩ Fin ) ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑤 ∈ 𝑣 ) → ( ( 𝑧 ∈ 𝑤 ∧ sup ( 𝑤 , ℝ* , < ) ≤ 𝑥 ) → 𝑧 ≤ 𝑥 ) )
146 145 rexlimdva ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝒫 ( (,) “ ( { -∞ } × ℝ ) ) ∩ Fin ) ) ∧ 𝑥 ∈ ℝ ) → ( ∃ 𝑤 ∈ 𝑣 ( 𝑧 ∈ 𝑤 ∧ sup ( 𝑤 , ℝ* , < ) ≤ 𝑥 ) → 𝑧 ≤ 𝑥 ) )
147 146 adantlrr ⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ ( 𝒫 ( (,) “ ( { -∞ } × ℝ ) ) ∩ Fin ) ∧ ran 𝐹 ⊆ ∪ 𝑣 ) ) ∧ 𝑥 ∈ ℝ ) → ( ∃ 𝑤 ∈ 𝑣 ( 𝑧 ∈ 𝑤 ∧ sup ( 𝑤 , ℝ* , < ) ≤ 𝑥 ) → 𝑧 ≤ 𝑥 ) )
148 125 147 syl5 ⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ ( 𝒫 ( (,) “ ( { -∞ } × ℝ ) ) ∩ Fin ) ∧ ran 𝐹 ⊆ ∪ 𝑣 ) ) ∧ 𝑥 ∈ ℝ ) → ( ( ∃ 𝑤 ∈ 𝑣 𝑧 ∈ 𝑤 ∧ ∀ 𝑤 ∈ 𝑣 sup ( 𝑤 , ℝ* , < ) ≤ 𝑥 ) → 𝑧 ≤ 𝑥 ) )
149 148 expdimp ⊢ ( ( ( ( 𝜑 ∧ ( 𝑣 ∈ ( 𝒫 ( (,) “ ( { -∞ } × ℝ ) ) ∩ Fin ) ∧ ran 𝐹 ⊆ ∪ 𝑣 ) ) ∧ 𝑥 ∈ ℝ ) ∧ ∃ 𝑤 ∈ 𝑣 𝑧 ∈ 𝑤 ) → ( ∀ 𝑤 ∈ 𝑣 sup ( 𝑤 , ℝ* , < ) ≤ 𝑥 → 𝑧 ≤ 𝑥 ) )
150 124 149 sylan2b ⊢ ( ( ( ( 𝜑 ∧ ( 𝑣 ∈ ( 𝒫 ( (,) “ ( { -∞ } × ℝ ) ) ∩ Fin ) ∧ ran 𝐹 ⊆ ∪ 𝑣 ) ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑧 ∈ ∪ 𝑣 ) → ( ∀ 𝑤 ∈ 𝑣 sup ( 𝑤 , ℝ* , < ) ≤ 𝑥 → 𝑧 ≤ 𝑥 ) )
151 123 150 syldan ⊢ ( ( ( ( 𝜑 ∧ ( 𝑣 ∈ ( 𝒫 ( (,) “ ( { -∞ } × ℝ ) ) ∩ Fin ) ∧ ran 𝐹 ⊆ ∪ 𝑣 ) ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑧 ∈ ran 𝐹 ) → ( ∀ 𝑤 ∈ 𝑣 sup ( 𝑤 , ℝ* , < ) ≤ 𝑥 → 𝑧 ≤ 𝑥 ) )
152 151 ralrimdva ⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ ( 𝒫 ( (,) “ ( { -∞ } × ℝ ) ) ∩ Fin ) ∧ ran 𝐹 ⊆ ∪ 𝑣 ) ) ∧ 𝑥 ∈ ℝ ) → ( ∀ 𝑤 ∈ 𝑣 sup ( 𝑤 , ℝ* , < ) ≤ 𝑥 → ∀ 𝑧 ∈ ran 𝐹 𝑧 ≤ 𝑥 ) )
153 9 ffnd ⊢ ( 𝜑 → 𝐹 Fn 𝑋 )
154 153 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ ( 𝒫 ( (,) “ ( { -∞ } × ℝ ) ) ∩ Fin ) ∧ ran 𝐹 ⊆ ∪ 𝑣 ) ) ∧ 𝑥 ∈ ℝ ) → 𝐹 Fn 𝑋 )
155 breq1 ⊢ ( 𝑧 = ( 𝐹 ‘ 𝑦 ) → ( 𝑧 ≤ 𝑥 ↔ ( 𝐹 ‘ 𝑦 ) ≤ 𝑥 ) )
156 155 ralrn ⊢ ( 𝐹 Fn 𝑋 → ( ∀ 𝑧 ∈ ran 𝐹 𝑧 ≤ 𝑥 ↔ ∀ 𝑦 ∈ 𝑋 ( 𝐹 ‘ 𝑦 ) ≤ 𝑥 ) )
157 154 156 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ ( 𝒫 ( (,) “ ( { -∞ } × ℝ ) ) ∩ Fin ) ∧ ran 𝐹 ⊆ ∪ 𝑣 ) ) ∧ 𝑥 ∈ ℝ ) → ( ∀ 𝑧 ∈ ran 𝐹 𝑧 ≤ 𝑥 ↔ ∀ 𝑦 ∈ 𝑋 ( 𝐹 ‘ 𝑦 ) ≤ 𝑥 ) )
158 152 157 sylibd ⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ ( 𝒫 ( (,) “ ( { -∞ } × ℝ ) ) ∩ Fin ) ∧ ran 𝐹 ⊆ ∪ 𝑣 ) ) ∧ 𝑥 ∈ ℝ ) → ( ∀ 𝑤 ∈ 𝑣 sup ( 𝑤 , ℝ* , < ) ≤ 𝑥 → ∀ 𝑦 ∈ 𝑋 ( 𝐹 ‘ 𝑦 ) ≤ 𝑥 ) )
159 158 reximdva ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( 𝒫 ( (,) “ ( { -∞ } × ℝ ) ) ∩ Fin ) ∧ ran 𝐹 ⊆ ∪ 𝑣 ) ) → ( ∃ 𝑥 ∈ ℝ ∀ 𝑤 ∈ 𝑣 sup ( 𝑤 , ℝ* , < ) ≤ 𝑥 → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝑋 ( 𝐹 ‘ 𝑦 ) ≤ 𝑥 ) )
160 121 159 mpd ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( 𝒫 ( (,) “ ( { -∞ } × ℝ ) ) ∩ Fin ) ∧ ran 𝐹 ⊆ ∪ 𝑣 ) ) → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝑋 ( 𝐹 ‘ 𝑦 ) ≤ 𝑥 )
161 68 160 rexlimddv ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝑋 ( 𝐹 ‘ 𝑦 ) ≤ 𝑥 )