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 elin ⊢ ( 𝑣 ∈ ( 𝒫 ( (,) “ ( { -∞ } × ℝ ) ) ∩ Fin ) ↔ ( 𝑣 ∈ 𝒫 ( (,) “ ( { -∞ } × ℝ ) ) ∧ 𝑣 ∈ Fin ) )
70 69 bilani ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 𝒫 ( (,) “ ( { -∞ } × ℝ ) ) ∩ Fin ) ) → ( 𝑣 ∈ 𝒫 ( (,) “ ( { -∞ } × ℝ ) ) ∧ 𝑣 ∈ Fin ) )
71 70 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( 𝒫 ( (,) “ ( { -∞ } × ℝ ) ) ∩ Fin ) ∧ ran 𝐹 ⊆ ∪ 𝑣 ) ) → ( 𝑣 ∈ 𝒫 ( (,) “ ( { -∞ } × ℝ ) ) ∧ 𝑣 ∈ Fin ) )
72 71 simprd ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( 𝒫 ( (,) “ ( { -∞ } × ℝ ) ) ∩ Fin ) ∧ ran 𝐹 ⊆ ∪ 𝑣 ) ) → 𝑣 ∈ Fin )
73 70 simpld ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 𝒫 ( (,) “ ( { -∞ } × ℝ ) ) ∩ Fin ) ) → 𝑣 ∈ 𝒫 ( (,) “ ( { -∞ } × ℝ ) ) )
74 73 elpwid ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 𝒫 ( (,) “ ( { -∞ } × ℝ ) ) ∩ Fin ) ) → 𝑣 ⊆ ( (,) “ ( { -∞ } × ℝ ) ) )
75 34 sseli ⊢ ( 𝑢 ∈ { -∞ } → 𝑢 ∈ ℝ* )
76 75 adantr ⊢ ( ( 𝑢 ∈ { -∞ } ∧ 𝑤 ∈ ℝ ) → 𝑢 ∈ ℝ* )
77 18 sseli ⊢ ( 𝑤 ∈ ℝ → 𝑤 ∈ ℝ* )
78 77 adantl ⊢ ( ( 𝑢 ∈ { -∞ } ∧ 𝑤 ∈ ℝ ) → 𝑤 ∈ ℝ* )
79 mnflt ⊢ ( 𝑤 ∈ ℝ → -∞ < 𝑤 )
80 xrltnle ⊢ ( ( -∞ ∈ ℝ* ∧ 𝑤 ∈ ℝ* ) → ( -∞ < 𝑤 ↔ ¬ 𝑤 ≤ -∞ ) )
81 25 77 80 sylancr ⊢ ( 𝑤 ∈ ℝ → ( -∞ < 𝑤 ↔ ¬ 𝑤 ≤ -∞ ) )
82 79 81 mpbid ⊢ ( 𝑤 ∈ ℝ → ¬ 𝑤 ≤ -∞ )
83 82 adantl ⊢ ( ( 𝑢 ∈ { -∞ } ∧ 𝑤 ∈ ℝ ) → ¬ 𝑤 ≤ -∞ )
84 elsni ⊢ ( 𝑢 ∈ { -∞ } → 𝑢 = -∞ )
85 84 adantr ⊢ ( ( 𝑢 ∈ { -∞ } ∧ 𝑤 ∈ ℝ ) → 𝑢 = -∞ )
86 85 breq2d ⊢ ( ( 𝑢 ∈ { -∞ } ∧ 𝑤 ∈ ℝ ) → ( 𝑤 ≤ 𝑢 ↔ 𝑤 ≤ -∞ ) )
87 83 86 mtbird ⊢ ( ( 𝑢 ∈ { -∞ } ∧ 𝑤 ∈ ℝ ) → ¬ 𝑤 ≤ 𝑢 )
88 ioo0 ⊢ ( ( 𝑢 ∈ ℝ* ∧ 𝑤 ∈ ℝ* ) → ( ( 𝑢 (,) 𝑤 ) = ∅ ↔ 𝑤 ≤ 𝑢 ) )
89 75 77 88 syl2an ⊢ ( ( 𝑢 ∈ { -∞ } ∧ 𝑤 ∈ ℝ ) → ( ( 𝑢 (,) 𝑤 ) = ∅ ↔ 𝑤 ≤ 𝑢 ) )
90 89 necon3abid ⊢ ( ( 𝑢 ∈ { -∞ } ∧ 𝑤 ∈ ℝ ) → ( ( 𝑢 (,) 𝑤 ) ≠ ∅ ↔ ¬ 𝑤 ≤ 𝑢 ) )
91 87 90 mpbird ⊢ ( ( 𝑢 ∈ { -∞ } ∧ 𝑤 ∈ ℝ ) → ( 𝑢 (,) 𝑤 ) ≠ ∅ )
92 df-ioo ⊢ (,) = ( 𝑦 ∈ ℝ* , 𝑧 ∈ ℝ* ↦ { 𝑣 ∈ ℝ* ∣ ( 𝑦 < 𝑣 ∧ 𝑣 < 𝑧 ) } )
93 idd ⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑤 ∈ ℝ* ) → ( 𝑥 < 𝑤 → 𝑥 < 𝑤 ) )
94 xrltle ⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑤 ∈ ℝ* ) → ( 𝑥 < 𝑤 → 𝑥 ≤ 𝑤 ) )
95 idd ⊢ ( ( 𝑢 ∈ ℝ* ∧ 𝑥 ∈ ℝ* ) → ( 𝑢 < 𝑥 → 𝑢 < 𝑥 ) )
96 xrltle ⊢ ( ( 𝑢 ∈ ℝ* ∧ 𝑥 ∈ ℝ* ) → ( 𝑢 < 𝑥 → 𝑢 ≤ 𝑥 ) )
97 92 93 94 95 96 ixxub ⊢ ( ( 𝑢 ∈ ℝ* ∧ 𝑤 ∈ ℝ* ∧ ( 𝑢 (,) 𝑤 ) ≠ ∅ ) → sup ( ( 𝑢 (,) 𝑤 ) , ℝ* , < ) = 𝑤 )
98 76 78 91 97 syl3anc ⊢ ( ( 𝑢 ∈ { -∞ } ∧ 𝑤 ∈ ℝ ) → sup ( ( 𝑢 (,) 𝑤 ) , ℝ* , < ) = 𝑤 )
99 simpr ⊢ ( ( 𝑢 ∈ { -∞ } ∧ 𝑤 ∈ ℝ ) → 𝑤 ∈ ℝ )
100 98 99 eqeltrd ⊢ ( ( 𝑢 ∈ { -∞ } ∧ 𝑤 ∈ ℝ ) → sup ( ( 𝑢 (,) 𝑤 ) , ℝ* , < ) ∈ ℝ )
101 100 rgen2 ⊢ ∀ 𝑢 ∈ { -∞ } ∀ 𝑤 ∈ ℝ sup ( ( 𝑢 (,) 𝑤 ) , ℝ* , < ) ∈ ℝ
102 fveq2 ⊢ ( 𝑧 = ⟨ 𝑢 , 𝑤 ⟩ → ( (,) ‘ 𝑧 ) = ( (,) ‘ ⟨ 𝑢 , 𝑤 ⟩ ) )
103 df-ov ⊢ ( 𝑢 (,) 𝑤 ) = ( (,) ‘ ⟨ 𝑢 , 𝑤 ⟩ )
104 102 103 eqtr4di ⊢ ( 𝑧 = ⟨ 𝑢 , 𝑤 ⟩ → ( (,) ‘ 𝑧 ) = ( 𝑢 (,) 𝑤 ) )
105 104 supeq1d ⊢ ( 𝑧 = ⟨ 𝑢 , 𝑤 ⟩ → sup ( ( (,) ‘ 𝑧 ) , ℝ* , < ) = sup ( ( 𝑢 (,) 𝑤 ) , ℝ* , < ) )
106 105 eleq1d ⊢ ( 𝑧 = ⟨ 𝑢 , 𝑤 ⟩ → ( sup ( ( (,) ‘ 𝑧 ) , ℝ* , < ) ∈ ℝ ↔ sup ( ( 𝑢 (,) 𝑤 ) , ℝ* , < ) ∈ ℝ ) )
107 106 ralxp ⊢ ( ∀ 𝑧 ∈ ( { -∞ } × ℝ ) sup ( ( (,) ‘ 𝑧 ) , ℝ* , < ) ∈ ℝ ↔ ∀ 𝑢 ∈ { -∞ } ∀ 𝑤 ∈ ℝ sup ( ( 𝑢 (,) 𝑤 ) , ℝ* , < ) ∈ ℝ )
108 101 107 mpbir ⊢ ∀ 𝑧 ∈ ( { -∞ } × ℝ ) sup ( ( (,) ‘ 𝑧 ) , ℝ* , < ) ∈ ℝ
109 ffn ⊢ ( (,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ → (,) Fn ( ℝ* × ℝ* ) )
110 30 109 ax-mp ⊢ (,) Fn ( ℝ* × ℝ* )
111 supeq1 ⊢ ( 𝑤 = ( (,) ‘ 𝑧 ) → sup ( 𝑤 , ℝ* , < ) = sup ( ( (,) ‘ 𝑧 ) , ℝ* , < ) )
112 111 eleq1d ⊢ ( 𝑤 = ( (,) ‘ 𝑧 ) → ( sup ( 𝑤 , ℝ* , < ) ∈ ℝ ↔ sup ( ( (,) ‘ 𝑧 ) , ℝ* , < ) ∈ ℝ ) )
113 112 ralima ⊢ ( ( (,) Fn ( ℝ* × ℝ* ) ∧ ( { -∞ } × ℝ ) ⊆ ( ℝ* × ℝ* ) ) → ( ∀ 𝑤 ∈ ( (,) “ ( { -∞ } × ℝ ) ) sup ( 𝑤 , ℝ* , < ) ∈ ℝ ↔ ∀ 𝑧 ∈ ( { -∞ } × ℝ ) sup ( ( (,) ‘ 𝑧 ) , ℝ* , < ) ∈ ℝ ) )
114 110 36 113 mp2an ⊢ ( ∀ 𝑤 ∈ ( (,) “ ( { -∞ } × ℝ ) ) sup ( 𝑤 , ℝ* , < ) ∈ ℝ ↔ ∀ 𝑧 ∈ ( { -∞ } × ℝ ) sup ( ( (,) ‘ 𝑧 ) , ℝ* , < ) ∈ ℝ )
115 108 114 mpbir ⊢ ∀ 𝑤 ∈ ( (,) “ ( { -∞ } × ℝ ) ) sup ( 𝑤 , ℝ* , < ) ∈ ℝ
116 ssralv ⊢ ( 𝑣 ⊆ ( (,) “ ( { -∞ } × ℝ ) ) → ( ∀ 𝑤 ∈ ( (,) “ ( { -∞ } × ℝ ) ) sup ( 𝑤 , ℝ* , < ) ∈ ℝ → ∀ 𝑤 ∈ 𝑣 sup ( 𝑤 , ℝ* , < ) ∈ ℝ ) )
117 74 115 116 mpisyl ⊢ ( ( 𝜑 ∧ 𝑣 ∈ ( 𝒫 ( (,) “ ( { -∞ } × ℝ ) ) ∩ Fin ) ) → ∀ 𝑤 ∈ 𝑣 sup ( 𝑤 , ℝ* , < ) ∈ ℝ )
118 117 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( 𝒫 ( (,) “ ( { -∞ } × ℝ ) ) ∩ Fin ) ∧ ran 𝐹 ⊆ ∪ 𝑣 ) ) → ∀ 𝑤 ∈ 𝑣 sup ( 𝑤 , ℝ* , < ) ∈ ℝ )
119 fimaxre3 ⊢ ( ( 𝑣 ∈ Fin ∧ ∀ 𝑤 ∈ 𝑣 sup ( 𝑤 , ℝ* , < ) ∈ ℝ ) → ∃ 𝑥 ∈ ℝ ∀ 𝑤 ∈ 𝑣 sup ( 𝑤 , ℝ* , < ) ≤ 𝑥 )
120 72 118 119 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( 𝒫 ( (,) “ ( { -∞ } × ℝ ) ) ∩ Fin ) ∧ ran 𝐹 ⊆ ∪ 𝑣 ) ) → ∃ 𝑥 ∈ ℝ ∀ 𝑤 ∈ 𝑣 sup ( 𝑤 , ℝ* , < ) ≤ 𝑥 )
121 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ ( 𝒫 ( (,) “ ( { -∞ } × ℝ ) ) ∩ Fin ) ∧ ran 𝐹 ⊆ ∪ 𝑣 ) ) ∧ 𝑥 ∈ ℝ ) → ran 𝐹 ⊆ ∪ 𝑣 )
122 121 sselda ⊢ ( ( ( ( 𝜑 ∧ ( 𝑣 ∈ ( 𝒫 ( (,) “ ( { -∞ } × ℝ ) ) ∩ Fin ) ∧ ran 𝐹 ⊆ ∪ 𝑣 ) ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑧 ∈ ran 𝐹 ) → 𝑧 ∈ ∪ 𝑣 )
123 eluni2 ⊢ ( 𝑧 ∈ ∪ 𝑣 ↔ ∃ 𝑤 ∈ 𝑣 𝑧 ∈ 𝑤 )
124 r19.29r ⊢ ( ( ∃ 𝑤 ∈ 𝑣 𝑧 ∈ 𝑤 ∧ ∀ 𝑤 ∈ 𝑣 sup ( 𝑤 , ℝ* , < ) ≤ 𝑥 ) → ∃ 𝑤 ∈ 𝑣 ( 𝑧 ∈ 𝑤 ∧ sup ( 𝑤 , ℝ* , < ) ≤ 𝑥 ) )
125 sspwuni ⊢ ( ( (,) “ ( { -∞ } × ℝ ) ) ⊆ 𝒫 ℝ ↔ ∪ ( (,) “ ( { -∞ } × ℝ ) ) ⊆ ℝ )
126 15 125 mpbir ⊢ ( (,) “ ( { -∞ } × ℝ ) ) ⊆ 𝒫 ℝ
127 74 3ad2ant1 ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝒫 ( (,) “ ( { -∞ } × ℝ ) ) ∩ Fin ) ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑤 ∈ 𝑣 ) ∧ ( 𝑧 ∈ 𝑤 ∧ sup ( 𝑤 , ℝ* , < ) ≤ 𝑥 ) ) → 𝑣 ⊆ ( (,) “ ( { -∞ } × ℝ ) ) )
128 simp2r ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝒫 ( (,) “ ( { -∞ } × ℝ ) ) ∩ Fin ) ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑤 ∈ 𝑣 ) ∧ ( 𝑧 ∈ 𝑤 ∧ sup ( 𝑤 , ℝ* , < ) ≤ 𝑥 ) ) → 𝑤 ∈ 𝑣 )
129 127 128 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝒫 ( (,) “ ( { -∞ } × ℝ ) ) ∩ Fin ) ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑤 ∈ 𝑣 ) ∧ ( 𝑧 ∈ 𝑤 ∧ sup ( 𝑤 , ℝ* , < ) ≤ 𝑥 ) ) → 𝑤 ∈ ( (,) “ ( { -∞ } × ℝ ) ) )
130 126 129 sselid ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝒫 ( (,) “ ( { -∞ } × ℝ ) ) ∩ Fin ) ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑤 ∈ 𝑣 ) ∧ ( 𝑧 ∈ 𝑤 ∧ sup ( 𝑤 , ℝ* , < ) ≤ 𝑥 ) ) → 𝑤 ∈ 𝒫 ℝ )
131 130 elpwid ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝒫 ( (,) “ ( { -∞ } × ℝ ) ) ∩ Fin ) ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑤 ∈ 𝑣 ) ∧ ( 𝑧 ∈ 𝑤 ∧ sup ( 𝑤 , ℝ* , < ) ≤ 𝑥 ) ) → 𝑤 ⊆ ℝ )
132 simp3l ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝒫 ( (,) “ ( { -∞ } × ℝ ) ) ∩ Fin ) ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑤 ∈ 𝑣 ) ∧ ( 𝑧 ∈ 𝑤 ∧ sup ( 𝑤 , ℝ* , < ) ≤ 𝑥 ) ) → 𝑧 ∈ 𝑤 )
133 131 132 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝒫 ( (,) “ ( { -∞ } × ℝ ) ) ∩ Fin ) ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑤 ∈ 𝑣 ) ∧ ( 𝑧 ∈ 𝑤 ∧ sup ( 𝑤 , ℝ* , < ) ≤ 𝑥 ) ) → 𝑧 ∈ ℝ )
134 117 r19.21bi ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝒫 ( (,) “ ( { -∞ } × ℝ ) ) ∩ Fin ) ) ∧ 𝑤 ∈ 𝑣 ) → sup ( 𝑤 , ℝ* , < ) ∈ ℝ )
135 134 adantrl ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝒫 ( (,) “ ( { -∞ } × ℝ ) ) ∩ Fin ) ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑤 ∈ 𝑣 ) ) → sup ( 𝑤 , ℝ* , < ) ∈ ℝ )
136 135 3adant3 ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝒫 ( (,) “ ( { -∞ } × ℝ ) ) ∩ Fin ) ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑤 ∈ 𝑣 ) ∧ ( 𝑧 ∈ 𝑤 ∧ sup ( 𝑤 , ℝ* , < ) ≤ 𝑥 ) ) → sup ( 𝑤 , ℝ* , < ) ∈ ℝ )
137 simp2l ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝒫 ( (,) “ ( { -∞ } × ℝ ) ) ∩ Fin ) ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑤 ∈ 𝑣 ) ∧ ( 𝑧 ∈ 𝑤 ∧ sup ( 𝑤 , ℝ* , < ) ≤ 𝑥 ) ) → 𝑥 ∈ ℝ )
138 131 18 sstrdi ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝒫 ( (,) “ ( { -∞ } × ℝ ) ) ∩ Fin ) ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑤 ∈ 𝑣 ) ∧ ( 𝑧 ∈ 𝑤 ∧ sup ( 𝑤 , ℝ* , < ) ≤ 𝑥 ) ) → 𝑤 ⊆ ℝ* )
139 supxrub ⊢ ( ( 𝑤 ⊆ ℝ* ∧ 𝑧 ∈ 𝑤 ) → 𝑧 ≤ sup ( 𝑤 , ℝ* , < ) )
140 138 132 139 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝒫 ( (,) “ ( { -∞ } × ℝ ) ) ∩ Fin ) ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑤 ∈ 𝑣 ) ∧ ( 𝑧 ∈ 𝑤 ∧ sup ( 𝑤 , ℝ* , < ) ≤ 𝑥 ) ) → 𝑧 ≤ sup ( 𝑤 , ℝ* , < ) )
141 simp3r ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝒫 ( (,) “ ( { -∞ } × ℝ ) ) ∩ Fin ) ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑤 ∈ 𝑣 ) ∧ ( 𝑧 ∈ 𝑤 ∧ sup ( 𝑤 , ℝ* , < ) ≤ 𝑥 ) ) → sup ( 𝑤 , ℝ* , < ) ≤ 𝑥 )
142 133 136 137 140 141 letrd ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝒫 ( (,) “ ( { -∞ } × ℝ ) ) ∩ Fin ) ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑤 ∈ 𝑣 ) ∧ ( 𝑧 ∈ 𝑤 ∧ sup ( 𝑤 , ℝ* , < ) ≤ 𝑥 ) ) → 𝑧 ≤ 𝑥 )
143 142 3expia ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝒫 ( (,) “ ( { -∞ } × ℝ ) ) ∩ Fin ) ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑤 ∈ 𝑣 ) ) → ( ( 𝑧 ∈ 𝑤 ∧ sup ( 𝑤 , ℝ* , < ) ≤ 𝑥 ) → 𝑧 ≤ 𝑥 ) )
144 143 anassrs ⊢ ( ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝒫 ( (,) “ ( { -∞ } × ℝ ) ) ∩ Fin ) ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑤 ∈ 𝑣 ) → ( ( 𝑧 ∈ 𝑤 ∧ sup ( 𝑤 , ℝ* , < ) ≤ 𝑥 ) → 𝑧 ≤ 𝑥 ) )
145 144 rexlimdva ⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ ( 𝒫 ( (,) “ ( { -∞ } × ℝ ) ) ∩ Fin ) ) ∧ 𝑥 ∈ ℝ ) → ( ∃ 𝑤 ∈ 𝑣 ( 𝑧 ∈ 𝑤 ∧ sup ( 𝑤 , ℝ* , < ) ≤ 𝑥 ) → 𝑧 ≤ 𝑥 ) )
146 145 adantlrr ⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ ( 𝒫 ( (,) “ ( { -∞ } × ℝ ) ) ∩ Fin ) ∧ ran 𝐹 ⊆ ∪ 𝑣 ) ) ∧ 𝑥 ∈ ℝ ) → ( ∃ 𝑤 ∈ 𝑣 ( 𝑧 ∈ 𝑤 ∧ sup ( 𝑤 , ℝ* , < ) ≤ 𝑥 ) → 𝑧 ≤ 𝑥 ) )
147 124 146 syl5 ⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ ( 𝒫 ( (,) “ ( { -∞ } × ℝ ) ) ∩ Fin ) ∧ ran 𝐹 ⊆ ∪ 𝑣 ) ) ∧ 𝑥 ∈ ℝ ) → ( ( ∃ 𝑤 ∈ 𝑣 𝑧 ∈ 𝑤 ∧ ∀ 𝑤 ∈ 𝑣 sup ( 𝑤 , ℝ* , < ) ≤ 𝑥 ) → 𝑧 ≤ 𝑥 ) )
148 147 expdimp ⊢ ( ( ( ( 𝜑 ∧ ( 𝑣 ∈ ( 𝒫 ( (,) “ ( { -∞ } × ℝ ) ) ∩ Fin ) ∧ ran 𝐹 ⊆ ∪ 𝑣 ) ) ∧ 𝑥 ∈ ℝ ) ∧ ∃ 𝑤 ∈ 𝑣 𝑧 ∈ 𝑤 ) → ( ∀ 𝑤 ∈ 𝑣 sup ( 𝑤 , ℝ* , < ) ≤ 𝑥 → 𝑧 ≤ 𝑥 ) )
149 123 148 sylan2b ⊢ ( ( ( ( 𝜑 ∧ ( 𝑣 ∈ ( 𝒫 ( (,) “ ( { -∞ } × ℝ ) ) ∩ Fin ) ∧ ran 𝐹 ⊆ ∪ 𝑣 ) ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑧 ∈ ∪ 𝑣 ) → ( ∀ 𝑤 ∈ 𝑣 sup ( 𝑤 , ℝ* , < ) ≤ 𝑥 → 𝑧 ≤ 𝑥 ) )
150 122 149 syldan ⊢ ( ( ( ( 𝜑 ∧ ( 𝑣 ∈ ( 𝒫 ( (,) “ ( { -∞ } × ℝ ) ) ∩ Fin ) ∧ ran 𝐹 ⊆ ∪ 𝑣 ) ) ∧ 𝑥 ∈ ℝ ) ∧ 𝑧 ∈ ran 𝐹 ) → ( ∀ 𝑤 ∈ 𝑣 sup ( 𝑤 , ℝ* , < ) ≤ 𝑥 → 𝑧 ≤ 𝑥 ) )
151 150 ralrimdva ⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ ( 𝒫 ( (,) “ ( { -∞ } × ℝ ) ) ∩ Fin ) ∧ ran 𝐹 ⊆ ∪ 𝑣 ) ) ∧ 𝑥 ∈ ℝ ) → ( ∀ 𝑤 ∈ 𝑣 sup ( 𝑤 , ℝ* , < ) ≤ 𝑥 → ∀ 𝑧 ∈ ran 𝐹 𝑧 ≤ 𝑥 ) )
152 9 ffnd ⊢ ( 𝜑 → 𝐹 Fn 𝑋 )
153 152 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ ( 𝒫 ( (,) “ ( { -∞ } × ℝ ) ) ∩ Fin ) ∧ ran 𝐹 ⊆ ∪ 𝑣 ) ) ∧ 𝑥 ∈ ℝ ) → 𝐹 Fn 𝑋 )
154 breq1 ⊢ ( 𝑧 = ( 𝐹 ‘ 𝑦 ) → ( 𝑧 ≤ 𝑥 ↔ ( 𝐹 ‘ 𝑦 ) ≤ 𝑥 ) )
155 154 ralrn ⊢ ( 𝐹 Fn 𝑋 → ( ∀ 𝑧 ∈ ran 𝐹 𝑧 ≤ 𝑥 ↔ ∀ 𝑦 ∈ 𝑋 ( 𝐹 ‘ 𝑦 ) ≤ 𝑥 ) )
156 153 155 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ ( 𝒫 ( (,) “ ( { -∞ } × ℝ ) ) ∩ Fin ) ∧ ran 𝐹 ⊆ ∪ 𝑣 ) ) ∧ 𝑥 ∈ ℝ ) → ( ∀ 𝑧 ∈ ran 𝐹 𝑧 ≤ 𝑥 ↔ ∀ 𝑦 ∈ 𝑋 ( 𝐹 ‘ 𝑦 ) ≤ 𝑥 ) )
157 151 156 sylibd ⊢ ( ( ( 𝜑 ∧ ( 𝑣 ∈ ( 𝒫 ( (,) “ ( { -∞ } × ℝ ) ) ∩ Fin ) ∧ ran 𝐹 ⊆ ∪ 𝑣 ) ) ∧ 𝑥 ∈ ℝ ) → ( ∀ 𝑤 ∈ 𝑣 sup ( 𝑤 , ℝ* , < ) ≤ 𝑥 → ∀ 𝑦 ∈ 𝑋 ( 𝐹 ‘ 𝑦 ) ≤ 𝑥 ) )
158 157 reximdva ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( 𝒫 ( (,) “ ( { -∞ } × ℝ ) ) ∩ Fin ) ∧ ran 𝐹 ⊆ ∪ 𝑣 ) ) → ( ∃ 𝑥 ∈ ℝ ∀ 𝑤 ∈ 𝑣 sup ( 𝑤 , ℝ* , < ) ≤ 𝑥 → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝑋 ( 𝐹 ‘ 𝑦 ) ≤ 𝑥 ) )
159 120 158 mpd ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( 𝒫 ( (,) “ ( { -∞ } × ℝ ) ) ∩ Fin ) ∧ ran 𝐹 ⊆ ∪ 𝑣 ) ) → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝑋 ( 𝐹 ‘ 𝑦 ) ≤ 𝑥 )
160 68 159 rexlimddv ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝑋 ( 𝐹 ‘ 𝑦 ) ≤ 𝑥 )