Metamath Proof Explorer

Theorem ssfiunibd

Description: A finite union of bounded sets is bounded. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses ssfiunibd.fi ⊢ ( 𝜑 → 𝐴 ∈ Fin )
ssfiunibd.b ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ∪ 𝐴 ) → 𝐵 ∈ ℝ )
ssfiunibd.bd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝑥 𝐵 ≤ 𝑦 )
ssfiunibd.ssun ⊢ ( 𝜑 → 𝐶 ⊆ ∪ 𝐴 )
Assertion ssfiunibd ( 𝜑 → ∃ 𝑤 ∈ ℝ ∀ 𝑧 ∈ 𝐶 𝐵 ≤ 𝑤 )

Proof

Step Hyp Ref Expression
1 ssfiunibd.fi ⊢ ( 𝜑 → 𝐴 ∈ Fin )
2 ssfiunibd.b ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ∪ 𝐴 ) → 𝐵 ∈ ℝ )
3 ssfiunibd.bd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝑥 𝐵 ≤ 𝑦 )
4 ssfiunibd.ssun ⊢ ( 𝜑 → 𝐶 ⊆ ∪ 𝐴 )
5 simpll ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝑥 ) → 𝜑 )
6 19.8a ⊢ ( ( 𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑥 ( 𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴 ) )
7 6 ancoms ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝑥 ) → ∃ 𝑥 ( 𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴 ) )
8 eluni ⊢ ( 𝑧 ∈ ∪ 𝐴 ↔ ∃ 𝑥 ( 𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴 ) )
9 7 8 sylibr ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝑥 ) → 𝑧 ∈ ∪ 𝐴 )
10 9 adantll ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝑥 ) → 𝑧 ∈ ∪ 𝐴 )
11 5 10 2 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝑥 ) → 𝐵 ∈ ℝ )
12 eqid ⊢ if ( 𝑥 = ∅ , 0 , sup ( { 𝑢 ∣ ∃ 𝑧 ∈ 𝑥 𝑢 = 𝐵 } , ℝ , < ) ) = if ( 𝑥 = ∅ , 0 , sup ( { 𝑢 ∣ ∃ 𝑧 ∈ 𝑥 𝑢 = 𝐵 } , ℝ , < ) )
13 11 3 12 upbdrech2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( if ( 𝑥 = ∅ , 0 , sup ( { 𝑢 ∣ ∃ 𝑧 ∈ 𝑥 𝑢 = 𝐵 } , ℝ , < ) ) ∈ ℝ ∧ ∀ 𝑧 ∈ 𝑥 𝐵 ≤ if ( 𝑥 = ∅ , 0 , sup ( { 𝑢 ∣ ∃ 𝑧 ∈ 𝑥 𝑢 = 𝐵 } , ℝ , < ) ) ) )
14 13 simpld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → if ( 𝑥 = ∅ , 0 , sup ( { 𝑢 ∣ ∃ 𝑧 ∈ 𝑥 𝑢 = 𝐵 } , ℝ , < ) ) ∈ ℝ )
15 14 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 if ( 𝑥 = ∅ , 0 , sup ( { 𝑢 ∣ ∃ 𝑧 ∈ 𝑥 𝑢 = 𝐵 } , ℝ , < ) ) ∈ ℝ )
16 fimaxre3 ⊢ ( ( 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 if ( 𝑥 = ∅ , 0 , sup ( { 𝑢 ∣ ∃ 𝑧 ∈ 𝑥 𝑢 = 𝐵 } , ℝ , < ) ) ∈ ℝ ) → ∃ 𝑤 ∈ ℝ ∀ 𝑥 ∈ 𝐴 if ( 𝑥 = ∅ , 0 , sup ( { 𝑢 ∣ ∃ 𝑧 ∈ 𝑥 𝑢 = 𝐵 } , ℝ , < ) ) ≤ 𝑤 )
17 1 15 16 syl2anc ⊢ ( 𝜑 → ∃ 𝑤 ∈ ℝ ∀ 𝑥 ∈ 𝐴 if ( 𝑥 = ∅ , 0 , sup ( { 𝑢 ∣ ∃ 𝑧 ∈ 𝑥 𝑢 = 𝐵 } , ℝ , < ) ) ≤ 𝑤 )
18 nfv ⊢ Ⅎ 𝑧 ( 𝜑 ∧ 𝑤 ∈ ℝ )
19 nfcv ⊢ Ⅎ 𝑧 𝐴
20 nfv ⊢ Ⅎ 𝑧 𝑥 = ∅
21 nfcv ⊢ Ⅎ 𝑧 0
22 nfre1 ⊢ Ⅎ 𝑧 ∃ 𝑧 ∈ 𝑥 𝑢 = 𝐵
23 22 nfab ⊢ Ⅎ 𝑧 { 𝑢 ∣ ∃ 𝑧 ∈ 𝑥 𝑢 = 𝐵 }
24 nfcv ⊢ Ⅎ 𝑧 ℝ
25 nfcv ⊢ Ⅎ 𝑧 <
26 23 24 25 nfsup ⊢ Ⅎ 𝑧 sup ( { 𝑢 ∣ ∃ 𝑧 ∈ 𝑥 𝑢 = 𝐵 } , ℝ , < )
27 20 21 26 nfif ⊢ Ⅎ 𝑧 if ( 𝑥 = ∅ , 0 , sup ( { 𝑢 ∣ ∃ 𝑧 ∈ 𝑥 𝑢 = 𝐵 } , ℝ , < ) )
28 nfcv ⊢ Ⅎ 𝑧 ≤
29 nfcv ⊢ Ⅎ 𝑧 𝑤
30 27 28 29 nfbr ⊢ Ⅎ 𝑧 if ( 𝑥 = ∅ , 0 , sup ( { 𝑢 ∣ ∃ 𝑧 ∈ 𝑥 𝑢 = 𝐵 } , ℝ , < ) ) ≤ 𝑤
31 19 30 nfralw ⊢ Ⅎ 𝑧 ∀ 𝑥 ∈ 𝐴 if ( 𝑥 = ∅ , 0 , sup ( { 𝑢 ∣ ∃ 𝑧 ∈ 𝑥 𝑢 = 𝐵 } , ℝ , < ) ) ≤ 𝑤
32 18 31 nfan ⊢ Ⅎ 𝑧 ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 if ( 𝑥 = ∅ , 0 , sup ( { 𝑢 ∣ ∃ 𝑧 ∈ 𝑥 𝑢 = 𝐵 } , ℝ , < ) ) ≤ 𝑤 )
33 4 sselda ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐶 ) → 𝑧 ∈ ∪ 𝐴 )
34 33 8 sylib ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐶 ) → ∃ 𝑥 ( 𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴 ) )
35 exancom ⊢ ( ∃ 𝑥 ( 𝑧 ∈ 𝑥 ∧ 𝑥 ∈ 𝐴 ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝑥 ) )
36 34 35 sylib ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐶 ) → ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝑥 ) )
37 df-rex ⊢ ( ∃ 𝑥 ∈ 𝐴 𝑧 ∈ 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝑥 ) )
38 36 37 sylibr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐶 ) → ∃ 𝑥 ∈ 𝐴 𝑧 ∈ 𝑥 )
39 38 ad4ant14 ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 if ( 𝑥 = ∅ , 0 , sup ( { 𝑢 ∣ ∃ 𝑧 ∈ 𝑥 𝑢 = 𝐵 } , ℝ , < ) ) ≤ 𝑤 ) ∧ 𝑧 ∈ 𝐶 ) → ∃ 𝑥 ∈ 𝐴 𝑧 ∈ 𝑥 )
40 nfv ⊢ Ⅎ 𝑥 ( 𝜑 ∧ 𝑤 ∈ ℝ )
41 nfra1 ⊢ Ⅎ 𝑥 ∀ 𝑥 ∈ 𝐴 if ( 𝑥 = ∅ , 0 , sup ( { 𝑢 ∣ ∃ 𝑧 ∈ 𝑥 𝑢 = 𝐵 } , ℝ , < ) ) ≤ 𝑤
42 40 41 nfan ⊢ Ⅎ 𝑥 ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 if ( 𝑥 = ∅ , 0 , sup ( { 𝑢 ∣ ∃ 𝑧 ∈ 𝑥 𝑢 = 𝐵 } , ℝ , < ) ) ≤ 𝑤 )
43 nfv ⊢ Ⅎ 𝑥 𝑧 ∈ 𝐶
44 42 43 nfan ⊢ Ⅎ 𝑥 ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 if ( 𝑥 = ∅ , 0 , sup ( { 𝑢 ∣ ∃ 𝑧 ∈ 𝑥 𝑢 = 𝐵 } , ℝ , < ) ) ≤ 𝑤 ) ∧ 𝑧 ∈ 𝐶 )
45 nfv ⊢ Ⅎ 𝑥 𝐵 ≤ 𝑤
46 11 3impa ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝑥 ) → 𝐵 ∈ ℝ )
47 46 3adant1r ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝑥 ) → 𝐵 ∈ ℝ )
48 47 3adant1r ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 if ( 𝑥 = ∅ , 0 , sup ( { 𝑢 ∣ ∃ 𝑧 ∈ 𝑥 𝑢 = 𝐵 } , ℝ , < ) ) ≤ 𝑤 ) ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝑥 ) → 𝐵 ∈ ℝ )
49 n0i ⊢ ( 𝑧 ∈ 𝑥 → ¬ 𝑥 = ∅ )
50 49 adantl ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝑥 ) → ¬ 𝑥 = ∅ )
51 50 iffalsed ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝑥 ) → if ( 𝑥 = ∅ , 0 , sup ( { 𝑢 ∣ ∃ 𝑧 ∈ 𝑥 𝑢 = 𝐵 } , ℝ , < ) ) = sup ( { 𝑢 ∣ ∃ 𝑧 ∈ 𝑥 𝑢 = 𝐵 } , ℝ , < ) )
52 51 eqcomd ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝑥 ) → sup ( { 𝑢 ∣ ∃ 𝑧 ∈ 𝑥 𝑢 = 𝐵 } , ℝ , < ) = if ( 𝑥 = ∅ , 0 , sup ( { 𝑢 ∣ ∃ 𝑧 ∈ 𝑥 𝑢 = 𝐵 } , ℝ , < ) ) )
53 52 3adant1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝑥 ) → sup ( { 𝑢 ∣ ∃ 𝑧 ∈ 𝑥 𝑢 = 𝐵 } , ℝ , < ) = if ( 𝑥 = ∅ , 0 , sup ( { 𝑢 ∣ ∃ 𝑧 ∈ 𝑥 𝑢 = 𝐵 } , ℝ , < ) ) )
54 14 3adant3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝑥 ) → if ( 𝑥 = ∅ , 0 , sup ( { 𝑢 ∣ ∃ 𝑧 ∈ 𝑥 𝑢 = 𝐵 } , ℝ , < ) ) ∈ ℝ )
55 53 54 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝑥 ) → sup ( { 𝑢 ∣ ∃ 𝑧 ∈ 𝑥 𝑢 = 𝐵 } , ℝ , < ) ∈ ℝ )
56 55 3adant1r ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝑥 ) → sup ( { 𝑢 ∣ ∃ 𝑧 ∈ 𝑥 𝑢 = 𝐵 } , ℝ , < ) ∈ ℝ )
57 56 3adant1r ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 if ( 𝑥 = ∅ , 0 , sup ( { 𝑢 ∣ ∃ 𝑧 ∈ 𝑥 𝑢 = 𝐵 } , ℝ , < ) ) ≤ 𝑤 ) ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝑥 ) → sup ( { 𝑢 ∣ ∃ 𝑧 ∈ 𝑥 𝑢 = 𝐵 } , ℝ , < ) ∈ ℝ )
58 simp1lr ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 if ( 𝑥 = ∅ , 0 , sup ( { 𝑢 ∣ ∃ 𝑧 ∈ 𝑥 𝑢 = 𝐵 } , ℝ , < ) ) ≤ 𝑤 ) ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝑥 ) → 𝑤 ∈ ℝ )
59 nfv ⊢ Ⅎ 𝑢 ( 𝜑 ∧ 𝑥 ∈ 𝐴 )
60 nfab1 ⊢ Ⅎ 𝑢 { 𝑢 ∣ ∃ 𝑧 ∈ 𝑥 𝑢 = 𝐵 }
61 nfcv ⊢ Ⅎ 𝑢 ℝ
62 abid ⊢ ( 𝑢 ∈ { 𝑢 ∣ ∃ 𝑧 ∈ 𝑥 𝑢 = 𝐵 } ↔ ∃ 𝑧 ∈ 𝑥 𝑢 = 𝐵 )
63 62 biimpi ⊢ ( 𝑢 ∈ { 𝑢 ∣ ∃ 𝑧 ∈ 𝑥 𝑢 = 𝐵 } → ∃ 𝑧 ∈ 𝑥 𝑢 = 𝐵 )
64 63 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑢 ∈ { 𝑢 ∣ ∃ 𝑧 ∈ 𝑥 𝑢 = 𝐵 } ) → ∃ 𝑧 ∈ 𝑥 𝑢 = 𝐵 )
65 nfv ⊢ Ⅎ 𝑧 ( 𝜑 ∧ 𝑥 ∈ 𝐴 )
66 22 nfsab ⊢ Ⅎ 𝑧 𝑢 ∈ { 𝑢 ∣ ∃ 𝑧 ∈ 𝑥 𝑢 = 𝐵 }
67 65 66 nfan ⊢ Ⅎ 𝑧 ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑢 ∈ { 𝑢 ∣ ∃ 𝑧 ∈ 𝑥 𝑢 = 𝐵 } )
68 nfv ⊢ Ⅎ 𝑧 𝑢 ∈ ℝ
69 simp3 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝑥 ∧ 𝑢 = 𝐵 ) → 𝑢 = 𝐵 )
70 11 3adant3 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝑥 ∧ 𝑢 = 𝐵 ) → 𝐵 ∈ ℝ )
71 69 70 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑧 ∈ 𝑥 ∧ 𝑢 = 𝐵 ) → 𝑢 ∈ ℝ )
72 71 3exp ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑧 ∈ 𝑥 → ( 𝑢 = 𝐵 → 𝑢 ∈ ℝ ) ) )
73 72 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑢 ∈ { 𝑢 ∣ ∃ 𝑧 ∈ 𝑥 𝑢 = 𝐵 } ) → ( 𝑧 ∈ 𝑥 → ( 𝑢 = 𝐵 → 𝑢 ∈ ℝ ) ) )
74 67 68 73 rexlimd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑢 ∈ { 𝑢 ∣ ∃ 𝑧 ∈ 𝑥 𝑢 = 𝐵 } ) → ( ∃ 𝑧 ∈ 𝑥 𝑢 = 𝐵 → 𝑢 ∈ ℝ ) )
75 64 74 mpd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑢 ∈ { 𝑢 ∣ ∃ 𝑧 ∈ 𝑥 𝑢 = 𝐵 } ) → 𝑢 ∈ ℝ )
76 75 ex ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑢 ∈ { 𝑢 ∣ ∃ 𝑧 ∈ 𝑥 𝑢 = 𝐵 } → 𝑢 ∈ ℝ ) )
77 59 60 61 76 ssrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → { 𝑢 ∣ ∃ 𝑧 ∈ 𝑥 𝑢 = 𝐵 } ⊆ ℝ )
78 77 3adant3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝑥 ) → { 𝑢 ∣ ∃ 𝑧 ∈ 𝑥 𝑢 = 𝐵 } ⊆ ℝ )
79 simp3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝑥 ) → 𝑧 ∈ 𝑥 )
80 elabrexg ⊢ ( ( 𝑧 ∈ 𝑥 ∧ 𝐵 ∈ ℝ ) → 𝐵 ∈ { 𝑢 ∣ ∃ 𝑧 ∈ 𝑥 𝑢 = 𝐵 } )
81 79 46 80 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝑥 ) → 𝐵 ∈ { 𝑢 ∣ ∃ 𝑧 ∈ 𝑥 𝑢 = 𝐵 } )
82 81 ne0d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝑥 ) → { 𝑢 ∣ ∃ 𝑧 ∈ 𝑥 𝑢 = 𝐵 } ≠ ∅ )
83 abid ⊢ ( 𝑣 ∈ { 𝑣 ∣ ∃ 𝑧 ∈ 𝑥 𝑣 = 𝐵 } ↔ ∃ 𝑧 ∈ 𝑥 𝑣 = 𝐵 )
84 83 biimpi ⊢ ( 𝑣 ∈ { 𝑣 ∣ ∃ 𝑧 ∈ 𝑥 𝑣 = 𝐵 } → ∃ 𝑧 ∈ 𝑥 𝑣 = 𝐵 )
85 eqeq1 ⊢ ( 𝑢 = 𝑣 → ( 𝑢 = 𝐵 ↔ 𝑣 = 𝐵 ) )
86 85 rexbidv ⊢ ( 𝑢 = 𝑣 → ( ∃ 𝑧 ∈ 𝑥 𝑢 = 𝐵 ↔ ∃ 𝑧 ∈ 𝑥 𝑣 = 𝐵 ) )
87 86 cbvabv ⊢ { 𝑢 ∣ ∃ 𝑧 ∈ 𝑥 𝑢 = 𝐵 } = { 𝑣 ∣ ∃ 𝑧 ∈ 𝑥 𝑣 = 𝐵 }
88 84 87 eleq2s ⊢ ( 𝑣 ∈ { 𝑢 ∣ ∃ 𝑧 ∈ 𝑥 𝑢 = 𝐵 } → ∃ 𝑧 ∈ 𝑥 𝑣 = 𝐵 )
89 88 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ ∀ 𝑧 ∈ 𝑥 𝐵 ≤ 𝑦 ) ∧ 𝑣 ∈ { 𝑢 ∣ ∃ 𝑧 ∈ 𝑥 𝑢 = 𝐵 } ) → ∃ 𝑧 ∈ 𝑥 𝑣 = 𝐵 )
90 nfra1 ⊢ Ⅎ 𝑧 ∀ 𝑧 ∈ 𝑥 𝐵 ≤ 𝑦
91 65 90 nfan ⊢ Ⅎ 𝑧 ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ ∀ 𝑧 ∈ 𝑥 𝐵 ≤ 𝑦 )
92 22 nfsab ⊢ Ⅎ 𝑧 𝑣 ∈ { 𝑢 ∣ ∃ 𝑧 ∈ 𝑥 𝑢 = 𝐵 }
93 91 92 nfan ⊢ Ⅎ 𝑧 ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ ∀ 𝑧 ∈ 𝑥 𝐵 ≤ 𝑦 ) ∧ 𝑣 ∈ { 𝑢 ∣ ∃ 𝑧 ∈ 𝑥 𝑢 = 𝐵 } )
94 nfv ⊢ Ⅎ 𝑧 𝑣 ≤ 𝑦
95 simp3 ⊢ ( ( ∀ 𝑧 ∈ 𝑥 𝐵 ≤ 𝑦 ∧ 𝑧 ∈ 𝑥 ∧ 𝑣 = 𝐵 ) → 𝑣 = 𝐵 )
96 rspa ⊢ ( ( ∀ 𝑧 ∈ 𝑥 𝐵 ≤ 𝑦 ∧ 𝑧 ∈ 𝑥 ) → 𝐵 ≤ 𝑦 )
97 96 3adant3 ⊢ ( ( ∀ 𝑧 ∈ 𝑥 𝐵 ≤ 𝑦 ∧ 𝑧 ∈ 𝑥 ∧ 𝑣 = 𝐵 ) → 𝐵 ≤ 𝑦 )
98 95 97 eqbrtrd ⊢ ( ( ∀ 𝑧 ∈ 𝑥 𝐵 ≤ 𝑦 ∧ 𝑧 ∈ 𝑥 ∧ 𝑣 = 𝐵 ) → 𝑣 ≤ 𝑦 )
99 98 3exp ⊢ ( ∀ 𝑧 ∈ 𝑥 𝐵 ≤ 𝑦 → ( 𝑧 ∈ 𝑥 → ( 𝑣 = 𝐵 → 𝑣 ≤ 𝑦 ) ) )
100 99 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ ∀ 𝑧 ∈ 𝑥 𝐵 ≤ 𝑦 ) → ( 𝑧 ∈ 𝑥 → ( 𝑣 = 𝐵 → 𝑣 ≤ 𝑦 ) ) )
101 100 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ ∀ 𝑧 ∈ 𝑥 𝐵 ≤ 𝑦 ) ∧ 𝑣 ∈ { 𝑢 ∣ ∃ 𝑧 ∈ 𝑥 𝑢 = 𝐵 } ) → ( 𝑧 ∈ 𝑥 → ( 𝑣 = 𝐵 → 𝑣 ≤ 𝑦 ) ) )
102 93 94 101 rexlimd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ ∀ 𝑧 ∈ 𝑥 𝐵 ≤ 𝑦 ) ∧ 𝑣 ∈ { 𝑢 ∣ ∃ 𝑧 ∈ 𝑥 𝑢 = 𝐵 } ) → ( ∃ 𝑧 ∈ 𝑥 𝑣 = 𝐵 → 𝑣 ≤ 𝑦 ) )
103 89 102 mpd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ ∀ 𝑧 ∈ 𝑥 𝐵 ≤ 𝑦 ) ∧ 𝑣 ∈ { 𝑢 ∣ ∃ 𝑧 ∈ 𝑥 𝑢 = 𝐵 } ) → 𝑣 ≤ 𝑦 )
104 103 ralrimiva ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ ∀ 𝑧 ∈ 𝑥 𝐵 ≤ 𝑦 ) → ∀ 𝑣 ∈ { 𝑢 ∣ ∃ 𝑧 ∈ 𝑥 𝑢 = 𝐵 } 𝑣 ≤ 𝑦 )
105 104 ex ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ∀ 𝑧 ∈ 𝑥 𝐵 ≤ 𝑦 → ∀ 𝑣 ∈ { 𝑢 ∣ ∃ 𝑧 ∈ 𝑥 𝑢 = 𝐵 } 𝑣 ≤ 𝑦 ) )
106 105 reximdv ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ∃ 𝑦 ∈ ℝ ∀ 𝑧 ∈ 𝑥 𝐵 ≤ 𝑦 → ∃ 𝑦 ∈ ℝ ∀ 𝑣 ∈ { 𝑢 ∣ ∃ 𝑧 ∈ 𝑥 𝑢 = 𝐵 } 𝑣 ≤ 𝑦 ) )
107 3 106 mpd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑦 ∈ ℝ ∀ 𝑣 ∈ { 𝑢 ∣ ∃ 𝑧 ∈ 𝑥 𝑢 = 𝐵 } 𝑣 ≤ 𝑦 )
108 107 3adant3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝑥 ) → ∃ 𝑦 ∈ ℝ ∀ 𝑣 ∈ { 𝑢 ∣ ∃ 𝑧 ∈ 𝑥 𝑢 = 𝐵 } 𝑣 ≤ 𝑦 )
109 suprub ⊢ ( ( ( { 𝑢 ∣ ∃ 𝑧 ∈ 𝑥 𝑢 = 𝐵 } ⊆ ℝ ∧ { 𝑢 ∣ ∃ 𝑧 ∈ 𝑥 𝑢 = 𝐵 } ≠ ∅ ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑣 ∈ { 𝑢 ∣ ∃ 𝑧 ∈ 𝑥 𝑢 = 𝐵 } 𝑣 ≤ 𝑦 ) ∧ 𝐵 ∈ { 𝑢 ∣ ∃ 𝑧 ∈ 𝑥 𝑢 = 𝐵 } ) → 𝐵 ≤ sup ( { 𝑢 ∣ ∃ 𝑧 ∈ 𝑥 𝑢 = 𝐵 } , ℝ , < ) )
110 78 82 108 81 109 syl31anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝑥 ) → 𝐵 ≤ sup ( { 𝑢 ∣ ∃ 𝑧 ∈ 𝑥 𝑢 = 𝐵 } , ℝ , < ) )
111 110 3adant1r ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝑥 ) → 𝐵 ≤ sup ( { 𝑢 ∣ ∃ 𝑧 ∈ 𝑥 𝑢 = 𝐵 } , ℝ , < ) )
112 111 3adant1r ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 if ( 𝑥 = ∅ , 0 , sup ( { 𝑢 ∣ ∃ 𝑧 ∈ 𝑥 𝑢 = 𝐵 } , ℝ , < ) ) ≤ 𝑤 ) ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝑥 ) → 𝐵 ≤ sup ( { 𝑢 ∣ ∃ 𝑧 ∈ 𝑥 𝑢 = 𝐵 } , ℝ , < ) )
113 52 3adant1 ⊢ ( ( ∀ 𝑥 ∈ 𝐴 if ( 𝑥 = ∅ , 0 , sup ( { 𝑢 ∣ ∃ 𝑧 ∈ 𝑥 𝑢 = 𝐵 } , ℝ , < ) ) ≤ 𝑤 ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝑥 ) → sup ( { 𝑢 ∣ ∃ 𝑧 ∈ 𝑥 𝑢 = 𝐵 } , ℝ , < ) = if ( 𝑥 = ∅ , 0 , sup ( { 𝑢 ∣ ∃ 𝑧 ∈ 𝑥 𝑢 = 𝐵 } , ℝ , < ) ) )
114 rspa ⊢ ( ( ∀ 𝑥 ∈ 𝐴 if ( 𝑥 = ∅ , 0 , sup ( { 𝑢 ∣ ∃ 𝑧 ∈ 𝑥 𝑢 = 𝐵 } , ℝ , < ) ) ≤ 𝑤 ∧ 𝑥 ∈ 𝐴 ) → if ( 𝑥 = ∅ , 0 , sup ( { 𝑢 ∣ ∃ 𝑧 ∈ 𝑥 𝑢 = 𝐵 } , ℝ , < ) ) ≤ 𝑤 )
115 114 3adant3 ⊢ ( ( ∀ 𝑥 ∈ 𝐴 if ( 𝑥 = ∅ , 0 , sup ( { 𝑢 ∣ ∃ 𝑧 ∈ 𝑥 𝑢 = 𝐵 } , ℝ , < ) ) ≤ 𝑤 ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝑥 ) → if ( 𝑥 = ∅ , 0 , sup ( { 𝑢 ∣ ∃ 𝑧 ∈ 𝑥 𝑢 = 𝐵 } , ℝ , < ) ) ≤ 𝑤 )
116 113 115 eqbrtrd ⊢ ( ( ∀ 𝑥 ∈ 𝐴 if ( 𝑥 = ∅ , 0 , sup ( { 𝑢 ∣ ∃ 𝑧 ∈ 𝑥 𝑢 = 𝐵 } , ℝ , < ) ) ≤ 𝑤 ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝑥 ) → sup ( { 𝑢 ∣ ∃ 𝑧 ∈ 𝑥 𝑢 = 𝐵 } , ℝ , < ) ≤ 𝑤 )
117 116 3adant1l ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 if ( 𝑥 = ∅ , 0 , sup ( { 𝑢 ∣ ∃ 𝑧 ∈ 𝑥 𝑢 = 𝐵 } , ℝ , < ) ) ≤ 𝑤 ) ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝑥 ) → sup ( { 𝑢 ∣ ∃ 𝑧 ∈ 𝑥 𝑢 = 𝐵 } , ℝ , < ) ≤ 𝑤 )
118 48 57 58 112 117 letrd ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 if ( 𝑥 = ∅ , 0 , sup ( { 𝑢 ∣ ∃ 𝑧 ∈ 𝑥 𝑢 = 𝐵 } , ℝ , < ) ) ≤ 𝑤 ) ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝑥 ) → 𝐵 ≤ 𝑤 )
119 118 3exp ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 if ( 𝑥 = ∅ , 0 , sup ( { 𝑢 ∣ ∃ 𝑧 ∈ 𝑥 𝑢 = 𝐵 } , ℝ , < ) ) ≤ 𝑤 ) → ( 𝑥 ∈ 𝐴 → ( 𝑧 ∈ 𝑥 → 𝐵 ≤ 𝑤 ) ) )
120 119 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 if ( 𝑥 = ∅ , 0 , sup ( { 𝑢 ∣ ∃ 𝑧 ∈ 𝑥 𝑢 = 𝐵 } , ℝ , < ) ) ≤ 𝑤 ) ∧ 𝑧 ∈ 𝐶 ) → ( 𝑥 ∈ 𝐴 → ( 𝑧 ∈ 𝑥 → 𝐵 ≤ 𝑤 ) ) )
121 44 45 120 rexlimd ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 if ( 𝑥 = ∅ , 0 , sup ( { 𝑢 ∣ ∃ 𝑧 ∈ 𝑥 𝑢 = 𝐵 } , ℝ , < ) ) ≤ 𝑤 ) ∧ 𝑧 ∈ 𝐶 ) → ( ∃ 𝑥 ∈ 𝐴 𝑧 ∈ 𝑥 → 𝐵 ≤ 𝑤 ) )
122 39 121 mpd ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 if ( 𝑥 = ∅ , 0 , sup ( { 𝑢 ∣ ∃ 𝑧 ∈ 𝑥 𝑢 = 𝐵 } , ℝ , < ) ) ≤ 𝑤 ) ∧ 𝑧 ∈ 𝐶 ) → 𝐵 ≤ 𝑤 )
123 122 ex ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 if ( 𝑥 = ∅ , 0 , sup ( { 𝑢 ∣ ∃ 𝑧 ∈ 𝑥 𝑢 = 𝐵 } , ℝ , < ) ) ≤ 𝑤 ) → ( 𝑧 ∈ 𝐶 → 𝐵 ≤ 𝑤 ) )
124 32 123 ralrimi ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ ∀ 𝑥 ∈ 𝐴 if ( 𝑥 = ∅ , 0 , sup ( { 𝑢 ∣ ∃ 𝑧 ∈ 𝑥 𝑢 = 𝐵 } , ℝ , < ) ) ≤ 𝑤 ) → ∀ 𝑧 ∈ 𝐶 𝐵 ≤ 𝑤 )
125 124 ex ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) → ( ∀ 𝑥 ∈ 𝐴 if ( 𝑥 = ∅ , 0 , sup ( { 𝑢 ∣ ∃ 𝑧 ∈ 𝑥 𝑢 = 𝐵 } , ℝ , < ) ) ≤ 𝑤 → ∀ 𝑧 ∈ 𝐶 𝐵 ≤ 𝑤 ) )
126 125 reximdva ⊢ ( 𝜑 → ( ∃ 𝑤 ∈ ℝ ∀ 𝑥 ∈ 𝐴 if ( 𝑥 = ∅ , 0 , sup ( { 𝑢 ∣ ∃ 𝑧 ∈ 𝑥 𝑢 = 𝐵 } , ℝ , < ) ) ≤ 𝑤 → ∃ 𝑤 ∈ ℝ ∀ 𝑧 ∈ 𝐶 𝐵 ≤ 𝑤 ) )
127 17 126 mpd ⊢ ( 𝜑 → ∃ 𝑤 ∈ ℝ ∀ 𝑧 ∈ 𝐶 𝐵 ≤ 𝑤 )