Metamath Proof Explorer

Theorem filbcmb

Description: Combine a finite set of lower bounds. (Contributed by Jeff Madsen, 2-Sep-2009)

Ref Expression
Assertion filbcmb ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐵 ⊆ ℝ ) → ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( 𝑦 ≤ 𝑧 → 𝜑 ) → ∃ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( 𝑦 ≤ 𝑧 → ∀ 𝑥 ∈ 𝐴 𝜑 ) ) )

Proof

Step Hyp Ref Expression
1 reex ⊢ ℝ ∈ V
2 1 ssex ⊢ ( 𝐵 ⊆ ℝ → 𝐵 ∈ V )
3 indexfi ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ V ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( 𝑦 ≤ 𝑧 → 𝜑 ) ) → ∃ 𝑤 ∈ Fin ( 𝑤 ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝑤 ∀ 𝑧 ∈ 𝐵 ( 𝑦 ≤ 𝑧 → 𝜑 ) ∧ ∀ 𝑦 ∈ 𝑤 ∃ 𝑥 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 ( 𝑦 ≤ 𝑧 → 𝜑 ) ) )
4 3 3expia ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ V ) → ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( 𝑦 ≤ 𝑧 → 𝜑 ) → ∃ 𝑤 ∈ Fin ( 𝑤 ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝑤 ∀ 𝑧 ∈ 𝐵 ( 𝑦 ≤ 𝑧 → 𝜑 ) ∧ ∀ 𝑦 ∈ 𝑤 ∃ 𝑥 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 ( 𝑦 ≤ 𝑧 → 𝜑 ) ) ) )
5 2 4 sylan2 ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ⊆ ℝ ) → ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( 𝑦 ≤ 𝑧 → 𝜑 ) → ∃ 𝑤 ∈ Fin ( 𝑤 ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝑤 ∀ 𝑧 ∈ 𝐵 ( 𝑦 ≤ 𝑧 → 𝜑 ) ∧ ∀ 𝑦 ∈ 𝑤 ∃ 𝑥 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 ( 𝑦 ≤ 𝑧 → 𝜑 ) ) ) )
6 5 3adant2 ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐵 ⊆ ℝ ) → ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( 𝑦 ≤ 𝑧 → 𝜑 ) → ∃ 𝑤 ∈ Fin ( 𝑤 ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝑤 ∀ 𝑧 ∈ 𝐵 ( 𝑦 ≤ 𝑧 → 𝜑 ) ∧ ∀ 𝑦 ∈ 𝑤 ∃ 𝑥 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 ( 𝑦 ≤ 𝑧 → 𝜑 ) ) ) )
7 r19.2z ⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝑤 ∀ 𝑧 ∈ 𝐵 ( 𝑦 ≤ 𝑧 → 𝜑 ) ) → ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝑤 ∀ 𝑧 ∈ 𝐵 ( 𝑦 ≤ 𝑧 → 𝜑 ) )
8 rexn0 ⊢ ( ∃ 𝑦 ∈ 𝑤 ∀ 𝑧 ∈ 𝐵 ( 𝑦 ≤ 𝑧 → 𝜑 ) → 𝑤 ≠ ∅ )
9 8 rexlimivw ⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝑤 ∀ 𝑧 ∈ 𝐵 ( 𝑦 ≤ 𝑧 → 𝜑 ) → 𝑤 ≠ ∅ )
10 7 9 syl ⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝑤 ∀ 𝑧 ∈ 𝐵 ( 𝑦 ≤ 𝑧 → 𝜑 ) ) → 𝑤 ≠ ∅ )
11 10 ex ⊢ ( 𝐴 ≠ ∅ → ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝑤 ∀ 𝑧 ∈ 𝐵 ( 𝑦 ≤ 𝑧 → 𝜑 ) → 𝑤 ≠ ∅ ) )
12 11 3ad2ant2 ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐵 ⊆ ℝ ) → ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝑤 ∀ 𝑧 ∈ 𝐵 ( 𝑦 ≤ 𝑧 → 𝜑 ) → 𝑤 ≠ ∅ ) )
13 12 ad2antrr ⊢ ( ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐵 ⊆ ℝ ) ∧ 𝑤 ∈ Fin ) ∧ 𝑤 ⊆ 𝐵 ) → ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝑤 ∀ 𝑧 ∈ 𝐵 ( 𝑦 ≤ 𝑧 → 𝜑 ) → 𝑤 ≠ ∅ ) )
14 sstr ⊢ ( ( 𝑤 ⊆ 𝐵 ∧ 𝐵 ⊆ ℝ ) → 𝑤 ⊆ ℝ )
15 14 ancoms ⊢ ( ( 𝐵 ⊆ ℝ ∧ 𝑤 ⊆ 𝐵 ) → 𝑤 ⊆ ℝ )
16 fimaxre ⊢ ( ( 𝑤 ⊆ ℝ ∧ 𝑤 ∈ Fin ∧ 𝑤 ≠ ∅ ) → ∃ 𝑦 ∈ 𝑤 ∀ 𝑢 ∈ 𝑤 𝑢 ≤ 𝑦 )
17 16 3expia ⊢ ( ( 𝑤 ⊆ ℝ ∧ 𝑤 ∈ Fin ) → ( 𝑤 ≠ ∅ → ∃ 𝑦 ∈ 𝑤 ∀ 𝑢 ∈ 𝑤 𝑢 ≤ 𝑦 ) )
18 15 17 sylan ⊢ ( ( ( 𝐵 ⊆ ℝ ∧ 𝑤 ⊆ 𝐵 ) ∧ 𝑤 ∈ Fin ) → ( 𝑤 ≠ ∅ → ∃ 𝑦 ∈ 𝑤 ∀ 𝑢 ∈ 𝑤 𝑢 ≤ 𝑦 ) )
19 18 anasss ⊢ ( ( 𝐵 ⊆ ℝ ∧ ( 𝑤 ⊆ 𝐵 ∧ 𝑤 ∈ Fin ) ) → ( 𝑤 ≠ ∅ → ∃ 𝑦 ∈ 𝑤 ∀ 𝑢 ∈ 𝑤 𝑢 ≤ 𝑦 ) )
20 19 ancom2s ⊢ ( ( 𝐵 ⊆ ℝ ∧ ( 𝑤 ∈ Fin ∧ 𝑤 ⊆ 𝐵 ) ) → ( 𝑤 ≠ ∅ → ∃ 𝑦 ∈ 𝑤 ∀ 𝑢 ∈ 𝑤 𝑢 ≤ 𝑦 ) )
21 20 3ad2antl3 ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐵 ⊆ ℝ ) ∧ ( 𝑤 ∈ Fin ∧ 𝑤 ⊆ 𝐵 ) ) → ( 𝑤 ≠ ∅ → ∃ 𝑦 ∈ 𝑤 ∀ 𝑢 ∈ 𝑤 𝑢 ≤ 𝑦 ) )
22 21 anassrs ⊢ ( ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐵 ⊆ ℝ ) ∧ 𝑤 ∈ Fin ) ∧ 𝑤 ⊆ 𝐵 ) → ( 𝑤 ≠ ∅ → ∃ 𝑦 ∈ 𝑤 ∀ 𝑢 ∈ 𝑤 𝑢 ≤ 𝑦 ) )
23 13 22 syld ⊢ ( ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐵 ⊆ ℝ ) ∧ 𝑤 ∈ Fin ) ∧ 𝑤 ⊆ 𝐵 ) → ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝑤 ∀ 𝑧 ∈ 𝐵 ( 𝑦 ≤ 𝑧 → 𝜑 ) → ∃ 𝑦 ∈ 𝑤 ∀ 𝑢 ∈ 𝑤 𝑢 ≤ 𝑦 ) )
24 23 a1dd ⊢ ( ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐵 ⊆ ℝ ) ∧ 𝑤 ∈ Fin ) ∧ 𝑤 ⊆ 𝐵 ) → ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝑤 ∀ 𝑧 ∈ 𝐵 ( 𝑦 ≤ 𝑧 → 𝜑 ) → ( ∀ 𝑦 ∈ 𝑤 ∃ 𝑥 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 ( 𝑦 ≤ 𝑧 → 𝜑 ) → ∃ 𝑦 ∈ 𝑤 ∀ 𝑢 ∈ 𝑤 𝑢 ≤ 𝑦 ) ) )
25 24 ex ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐵 ⊆ ℝ ) ∧ 𝑤 ∈ Fin ) → ( 𝑤 ⊆ 𝐵 → ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝑤 ∀ 𝑧 ∈ 𝐵 ( 𝑦 ≤ 𝑧 → 𝜑 ) → ( ∀ 𝑦 ∈ 𝑤 ∃ 𝑥 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 ( 𝑦 ≤ 𝑧 → 𝜑 ) → ∃ 𝑦 ∈ 𝑤 ∀ 𝑢 ∈ 𝑤 𝑢 ≤ 𝑦 ) ) ) )
26 25 3impd ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐵 ⊆ ℝ ) ∧ 𝑤 ∈ Fin ) → ( ( 𝑤 ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝑤 ∀ 𝑧 ∈ 𝐵 ( 𝑦 ≤ 𝑧 → 𝜑 ) ∧ ∀ 𝑦 ∈ 𝑤 ∃ 𝑥 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 ( 𝑦 ≤ 𝑧 → 𝜑 ) ) → ∃ 𝑦 ∈ 𝑤 ∀ 𝑢 ∈ 𝑤 𝑢 ≤ 𝑦 ) )
27 nfv ⊢ Ⅎ 𝑦 ( 𝐵 ⊆ ℝ ∧ 𝑤 ⊆ 𝐵 )
28 nfcv ⊢ Ⅎ 𝑦 𝐴
29 nfre1 ⊢ Ⅎ 𝑦 ∃ 𝑦 ∈ 𝑤 ∀ 𝑧 ∈ 𝐵 ( 𝑦 ≤ 𝑧 → 𝜑 )
30 28 29 nfralw ⊢ Ⅎ 𝑦 ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝑤 ∀ 𝑧 ∈ 𝐵 ( 𝑦 ≤ 𝑧 → 𝜑 )
31 27 30 nfan ⊢ Ⅎ 𝑦 ( ( 𝐵 ⊆ ℝ ∧ 𝑤 ⊆ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝑤 ∀ 𝑧 ∈ 𝐵 ( 𝑦 ≤ 𝑧 → 𝜑 ) )
32 nfv ⊢ Ⅎ 𝑧 ( 𝐵 ⊆ ℝ ∧ 𝑤 ⊆ 𝐵 )
33 nfcv ⊢ Ⅎ 𝑧 𝐴
34 nfcv ⊢ Ⅎ 𝑧 𝑤
35 nfra1 ⊢ Ⅎ 𝑧 ∀ 𝑧 ∈ 𝐵 ( 𝑦 ≤ 𝑧 → 𝜑 )
36 34 35 nfrexw ⊢ Ⅎ 𝑧 ∃ 𝑦 ∈ 𝑤 ∀ 𝑧 ∈ 𝐵 ( 𝑦 ≤ 𝑧 → 𝜑 )
37 33 36 nfralw ⊢ Ⅎ 𝑧 ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝑤 ∀ 𝑧 ∈ 𝐵 ( 𝑦 ≤ 𝑧 → 𝜑 )
38 32 37 nfan ⊢ Ⅎ 𝑧 ( ( 𝐵 ⊆ ℝ ∧ 𝑤 ⊆ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝑤 ∀ 𝑧 ∈ 𝐵 ( 𝑦 ≤ 𝑧 → 𝜑 ) )
39 nfv ⊢ Ⅎ 𝑧 ( 𝑦 ∈ 𝑤 ∧ ∀ 𝑢 ∈ 𝑤 𝑢 ≤ 𝑦 )
40 38 39 nfan ⊢ Ⅎ 𝑧 ( ( ( 𝐵 ⊆ ℝ ∧ 𝑤 ⊆ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝑤 ∀ 𝑧 ∈ 𝐵 ( 𝑦 ≤ 𝑧 → 𝜑 ) ) ∧ ( 𝑦 ∈ 𝑤 ∧ ∀ 𝑢 ∈ 𝑤 𝑢 ≤ 𝑦 ) )
41 breq1 ⊢ ( 𝑦 = 𝑣 → ( 𝑦 ≤ 𝑧 ↔ 𝑣 ≤ 𝑧 ) )
42 41 imbi1d ⊢ ( 𝑦 = 𝑣 → ( ( 𝑦 ≤ 𝑧 → 𝜑 ) ↔ ( 𝑣 ≤ 𝑧 → 𝜑 ) ) )
43 42 ralbidv ⊢ ( 𝑦 = 𝑣 → ( ∀ 𝑧 ∈ 𝐵 ( 𝑦 ≤ 𝑧 → 𝜑 ) ↔ ∀ 𝑧 ∈ 𝐵 ( 𝑣 ≤ 𝑧 → 𝜑 ) ) )
44 43 cbvrexvw ⊢ ( ∃ 𝑦 ∈ 𝑤 ∀ 𝑧 ∈ 𝐵 ( 𝑦 ≤ 𝑧 → 𝜑 ) ↔ ∃ 𝑣 ∈ 𝑤 ∀ 𝑧 ∈ 𝐵 ( 𝑣 ≤ 𝑧 → 𝜑 ) )
45 rsp ⊢ ( ∀ 𝑧 ∈ 𝐵 ( 𝑣 ≤ 𝑧 → 𝜑 ) → ( 𝑧 ∈ 𝐵 → ( 𝑣 ≤ 𝑧 → 𝜑 ) ) )
46 ssel2 ⊢ ( ( 𝑤 ⊆ 𝐵 ∧ 𝑣 ∈ 𝑤 ) → 𝑣 ∈ 𝐵 )
47 ssel2 ⊢ ( ( 𝐵 ⊆ ℝ ∧ 𝑣 ∈ 𝐵 ) → 𝑣 ∈ ℝ )
48 46 47 sylan2 ⊢ ( ( 𝐵 ⊆ ℝ ∧ ( 𝑤 ⊆ 𝐵 ∧ 𝑣 ∈ 𝑤 ) ) → 𝑣 ∈ ℝ )
49 48 anassrs ⊢ ( ( ( 𝐵 ⊆ ℝ ∧ 𝑤 ⊆ 𝐵 ) ∧ 𝑣 ∈ 𝑤 ) → 𝑣 ∈ ℝ )
50 49 adantlr ⊢ ( ( ( ( 𝐵 ⊆ ℝ ∧ 𝑤 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ∀ 𝑢 ∈ 𝑤 𝑢 ≤ 𝑦 ) ) ∧ 𝑣 ∈ 𝑤 ) → 𝑣 ∈ ℝ )
51 50 adantlr ⊢ ( ( ( ( ( 𝐵 ⊆ ℝ ∧ 𝑤 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ∀ 𝑢 ∈ 𝑤 𝑢 ≤ 𝑦 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑦 ≤ 𝑧 ) ) ∧ 𝑣 ∈ 𝑤 ) → 𝑣 ∈ ℝ )
52 ssel2 ⊢ ( ( 𝑤 ⊆ 𝐵 ∧ 𝑦 ∈ 𝑤 ) → 𝑦 ∈ 𝐵 )
53 ssel2 ⊢ ( ( 𝐵 ⊆ ℝ ∧ 𝑦 ∈ 𝐵 ) → 𝑦 ∈ ℝ )
54 52 53 sylan2 ⊢ ( ( 𝐵 ⊆ ℝ ∧ ( 𝑤 ⊆ 𝐵 ∧ 𝑦 ∈ 𝑤 ) ) → 𝑦 ∈ ℝ )
55 54 anassrs ⊢ ( ( ( 𝐵 ⊆ ℝ ∧ 𝑤 ⊆ 𝐵 ) ∧ 𝑦 ∈ 𝑤 ) → 𝑦 ∈ ℝ )
56 55 adantrr ⊢ ( ( ( 𝐵 ⊆ ℝ ∧ 𝑤 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ∀ 𝑢 ∈ 𝑤 𝑢 ≤ 𝑦 ) ) → 𝑦 ∈ ℝ )
57 56 ad2antrr ⊢ ( ( ( ( ( 𝐵 ⊆ ℝ ∧ 𝑤 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ∀ 𝑢 ∈ 𝑤 𝑢 ≤ 𝑦 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑦 ≤ 𝑧 ) ) ∧ 𝑣 ∈ 𝑤 ) → 𝑦 ∈ ℝ )
58 ssel2 ⊢ ( ( 𝐵 ⊆ ℝ ∧ 𝑧 ∈ 𝐵 ) → 𝑧 ∈ ℝ )
59 58 adantlr ⊢ ( ( ( 𝐵 ⊆ ℝ ∧ 𝑤 ⊆ 𝐵 ) ∧ 𝑧 ∈ 𝐵 ) → 𝑧 ∈ ℝ )
60 59 ad2ant2r ⊢ ( ( ( ( 𝐵 ⊆ ℝ ∧ 𝑤 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ∀ 𝑢 ∈ 𝑤 𝑢 ≤ 𝑦 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑦 ≤ 𝑧 ) ) → 𝑧 ∈ ℝ )
61 60 adantr ⊢ ( ( ( ( ( 𝐵 ⊆ ℝ ∧ 𝑤 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ∀ 𝑢 ∈ 𝑤 𝑢 ≤ 𝑦 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑦 ≤ 𝑧 ) ) ∧ 𝑣 ∈ 𝑤 ) → 𝑧 ∈ ℝ )
62 breq1 ⊢ ( 𝑢 = 𝑣 → ( 𝑢 ≤ 𝑦 ↔ 𝑣 ≤ 𝑦 ) )
63 62 rspccva ⊢ ( ( ∀ 𝑢 ∈ 𝑤 𝑢 ≤ 𝑦 ∧ 𝑣 ∈ 𝑤 ) → 𝑣 ≤ 𝑦 )
64 63 adantll ⊢ ( ( ( 𝑦 ∈ 𝑤 ∧ ∀ 𝑢 ∈ 𝑤 𝑢 ≤ 𝑦 ) ∧ 𝑣 ∈ 𝑤 ) → 𝑣 ≤ 𝑦 )
65 64 adantll ⊢ ( ( ( ( 𝐵 ⊆ ℝ ∧ 𝑤 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ∀ 𝑢 ∈ 𝑤 𝑢 ≤ 𝑦 ) ) ∧ 𝑣 ∈ 𝑤 ) → 𝑣 ≤ 𝑦 )
66 65 adantlr ⊢ ( ( ( ( ( 𝐵 ⊆ ℝ ∧ 𝑤 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ∀ 𝑢 ∈ 𝑤 𝑢 ≤ 𝑦 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑦 ≤ 𝑧 ) ) ∧ 𝑣 ∈ 𝑤 ) → 𝑣 ≤ 𝑦 )
67 simplrr ⊢ ( ( ( ( ( 𝐵 ⊆ ℝ ∧ 𝑤 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ∀ 𝑢 ∈ 𝑤 𝑢 ≤ 𝑦 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑦 ≤ 𝑧 ) ) ∧ 𝑣 ∈ 𝑤 ) → 𝑦 ≤ 𝑧 )
68 51 57 61 66 67 letrd ⊢ ( ( ( ( ( 𝐵 ⊆ ℝ ∧ 𝑤 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ∀ 𝑢 ∈ 𝑤 𝑢 ≤ 𝑦 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑦 ≤ 𝑧 ) ) ∧ 𝑣 ∈ 𝑤 ) → 𝑣 ≤ 𝑧 )
69 pm2.27 ⊢ ( 𝑧 ∈ 𝐵 → ( ( 𝑧 ∈ 𝐵 → ( 𝑣 ≤ 𝑧 → 𝜑 ) ) → ( 𝑣 ≤ 𝑧 → 𝜑 ) ) )
70 69 adantr ⊢ ( ( 𝑧 ∈ 𝐵 ∧ 𝑦 ≤ 𝑧 ) → ( ( 𝑧 ∈ 𝐵 → ( 𝑣 ≤ 𝑧 → 𝜑 ) ) → ( 𝑣 ≤ 𝑧 → 𝜑 ) ) )
71 70 ad2antlr ⊢ ( ( ( ( ( 𝐵 ⊆ ℝ ∧ 𝑤 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ∀ 𝑢 ∈ 𝑤 𝑢 ≤ 𝑦 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑦 ≤ 𝑧 ) ) ∧ 𝑣 ∈ 𝑤 ) → ( ( 𝑧 ∈ 𝐵 → ( 𝑣 ≤ 𝑧 → 𝜑 ) ) → ( 𝑣 ≤ 𝑧 → 𝜑 ) ) )
72 68 71 mpid ⊢ ( ( ( ( ( 𝐵 ⊆ ℝ ∧ 𝑤 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ∀ 𝑢 ∈ 𝑤 𝑢 ≤ 𝑦 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑦 ≤ 𝑧 ) ) ∧ 𝑣 ∈ 𝑤 ) → ( ( 𝑧 ∈ 𝐵 → ( 𝑣 ≤ 𝑧 → 𝜑 ) ) → 𝜑 ) )
73 45 72 syl5 ⊢ ( ( ( ( ( 𝐵 ⊆ ℝ ∧ 𝑤 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ∀ 𝑢 ∈ 𝑤 𝑢 ≤ 𝑦 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑦 ≤ 𝑧 ) ) ∧ 𝑣 ∈ 𝑤 ) → ( ∀ 𝑧 ∈ 𝐵 ( 𝑣 ≤ 𝑧 → 𝜑 ) → 𝜑 ) )
74 73 adantlr ⊢ ( ( ( ( ( ( 𝐵 ⊆ ℝ ∧ 𝑤 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ∀ 𝑢 ∈ 𝑤 𝑢 ≤ 𝑦 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑦 ≤ 𝑧 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑣 ∈ 𝑤 ) → ( ∀ 𝑧 ∈ 𝐵 ( 𝑣 ≤ 𝑧 → 𝜑 ) → 𝜑 ) )
75 74 rexlimdva ⊢ ( ( ( ( ( 𝐵 ⊆ ℝ ∧ 𝑤 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ∀ 𝑢 ∈ 𝑤 𝑢 ≤ 𝑦 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑦 ≤ 𝑧 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( ∃ 𝑣 ∈ 𝑤 ∀ 𝑧 ∈ 𝐵 ( 𝑣 ≤ 𝑧 → 𝜑 ) → 𝜑 ) )
76 44 75 biimtrid ⊢ ( ( ( ( ( 𝐵 ⊆ ℝ ∧ 𝑤 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ∀ 𝑢 ∈ 𝑤 𝑢 ≤ 𝑦 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑦 ≤ 𝑧 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( ∃ 𝑦 ∈ 𝑤 ∀ 𝑧 ∈ 𝐵 ( 𝑦 ≤ 𝑧 → 𝜑 ) → 𝜑 ) )
77 76 ralimdva ⊢ ( ( ( ( 𝐵 ⊆ ℝ ∧ 𝑤 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ∀ 𝑢 ∈ 𝑤 𝑢 ≤ 𝑦 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑦 ≤ 𝑧 ) ) → ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝑤 ∀ 𝑧 ∈ 𝐵 ( 𝑦 ≤ 𝑧 → 𝜑 ) → ∀ 𝑥 ∈ 𝐴 𝜑 ) )
78 77 imp ⊢ ( ( ( ( ( 𝐵 ⊆ ℝ ∧ 𝑤 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ∀ 𝑢 ∈ 𝑤 𝑢 ≤ 𝑦 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑦 ≤ 𝑧 ) ) ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝑤 ∀ 𝑧 ∈ 𝐵 ( 𝑦 ≤ 𝑧 → 𝜑 ) ) → ∀ 𝑥 ∈ 𝐴 𝜑 )
79 78 an32s ⊢ ( ( ( ( ( 𝐵 ⊆ ℝ ∧ 𝑤 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ∀ 𝑢 ∈ 𝑤 𝑢 ≤ 𝑦 ) ) ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝑤 ∀ 𝑧 ∈ 𝐵 ( 𝑦 ≤ 𝑧 → 𝜑 ) ) ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑦 ≤ 𝑧 ) ) → ∀ 𝑥 ∈ 𝐴 𝜑 )
80 79 exp32 ⊢ ( ( ( ( 𝐵 ⊆ ℝ ∧ 𝑤 ⊆ 𝐵 ) ∧ ( 𝑦 ∈ 𝑤 ∧ ∀ 𝑢 ∈ 𝑤 𝑢 ≤ 𝑦 ) ) ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝑤 ∀ 𝑧 ∈ 𝐵 ( 𝑦 ≤ 𝑧 → 𝜑 ) ) → ( 𝑧 ∈ 𝐵 → ( 𝑦 ≤ 𝑧 → ∀ 𝑥 ∈ 𝐴 𝜑 ) ) )
81 80 an32s ⊢ ( ( ( ( 𝐵 ⊆ ℝ ∧ 𝑤 ⊆ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝑤 ∀ 𝑧 ∈ 𝐵 ( 𝑦 ≤ 𝑧 → 𝜑 ) ) ∧ ( 𝑦 ∈ 𝑤 ∧ ∀ 𝑢 ∈ 𝑤 𝑢 ≤ 𝑦 ) ) → ( 𝑧 ∈ 𝐵 → ( 𝑦 ≤ 𝑧 → ∀ 𝑥 ∈ 𝐴 𝜑 ) ) )
82 40 81 ralrimi ⊢ ( ( ( ( 𝐵 ⊆ ℝ ∧ 𝑤 ⊆ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝑤 ∀ 𝑧 ∈ 𝐵 ( 𝑦 ≤ 𝑧 → 𝜑 ) ) ∧ ( 𝑦 ∈ 𝑤 ∧ ∀ 𝑢 ∈ 𝑤 𝑢 ≤ 𝑦 ) ) → ∀ 𝑧 ∈ 𝐵 ( 𝑦 ≤ 𝑧 → ∀ 𝑥 ∈ 𝐴 𝜑 ) )
83 82 exp32 ⊢ ( ( ( 𝐵 ⊆ ℝ ∧ 𝑤 ⊆ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝑤 ∀ 𝑧 ∈ 𝐵 ( 𝑦 ≤ 𝑧 → 𝜑 ) ) → ( 𝑦 ∈ 𝑤 → ( ∀ 𝑢 ∈ 𝑤 𝑢 ≤ 𝑦 → ∀ 𝑧 ∈ 𝐵 ( 𝑦 ≤ 𝑧 → ∀ 𝑥 ∈ 𝐴 𝜑 ) ) ) )
84 31 83 reximdai ⊢ ( ( ( 𝐵 ⊆ ℝ ∧ 𝑤 ⊆ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝑤 ∀ 𝑧 ∈ 𝐵 ( 𝑦 ≤ 𝑧 → 𝜑 ) ) → ( ∃ 𝑦 ∈ 𝑤 ∀ 𝑢 ∈ 𝑤 𝑢 ≤ 𝑦 → ∃ 𝑦 ∈ 𝑤 ∀ 𝑧 ∈ 𝐵 ( 𝑦 ≤ 𝑧 → ∀ 𝑥 ∈ 𝐴 𝜑 ) ) )
85 84 adantrr ⊢ ( ( ( 𝐵 ⊆ ℝ ∧ 𝑤 ⊆ 𝐵 ) ∧ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝑤 ∀ 𝑧 ∈ 𝐵 ( 𝑦 ≤ 𝑧 → 𝜑 ) ∧ ∀ 𝑦 ∈ 𝑤 ∃ 𝑥 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 ( 𝑦 ≤ 𝑧 → 𝜑 ) ) ) → ( ∃ 𝑦 ∈ 𝑤 ∀ 𝑢 ∈ 𝑤 𝑢 ≤ 𝑦 → ∃ 𝑦 ∈ 𝑤 ∀ 𝑧 ∈ 𝐵 ( 𝑦 ≤ 𝑧 → ∀ 𝑥 ∈ 𝐴 𝜑 ) ) )
86 ssrexv ⊢ ( 𝑤 ⊆ 𝐵 → ( ∃ 𝑦 ∈ 𝑤 ∀ 𝑧 ∈ 𝐵 ( 𝑦 ≤ 𝑧 → ∀ 𝑥 ∈ 𝐴 𝜑 ) → ∃ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( 𝑦 ≤ 𝑧 → ∀ 𝑥 ∈ 𝐴 𝜑 ) ) )
87 86 ad2antlr ⊢ ( ( ( 𝐵 ⊆ ℝ ∧ 𝑤 ⊆ 𝐵 ) ∧ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝑤 ∀ 𝑧 ∈ 𝐵 ( 𝑦 ≤ 𝑧 → 𝜑 ) ∧ ∀ 𝑦 ∈ 𝑤 ∃ 𝑥 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 ( 𝑦 ≤ 𝑧 → 𝜑 ) ) ) → ( ∃ 𝑦 ∈ 𝑤 ∀ 𝑧 ∈ 𝐵 ( 𝑦 ≤ 𝑧 → ∀ 𝑥 ∈ 𝐴 𝜑 ) → ∃ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( 𝑦 ≤ 𝑧 → ∀ 𝑥 ∈ 𝐴 𝜑 ) ) )
88 85 87 syld ⊢ ( ( ( 𝐵 ⊆ ℝ ∧ 𝑤 ⊆ 𝐵 ) ∧ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝑤 ∀ 𝑧 ∈ 𝐵 ( 𝑦 ≤ 𝑧 → 𝜑 ) ∧ ∀ 𝑦 ∈ 𝑤 ∃ 𝑥 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 ( 𝑦 ≤ 𝑧 → 𝜑 ) ) ) → ( ∃ 𝑦 ∈ 𝑤 ∀ 𝑢 ∈ 𝑤 𝑢 ≤ 𝑦 → ∃ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( 𝑦 ≤ 𝑧 → ∀ 𝑥 ∈ 𝐴 𝜑 ) ) )
89 88 exp43 ⊢ ( 𝐵 ⊆ ℝ → ( 𝑤 ⊆ 𝐵 → ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝑤 ∀ 𝑧 ∈ 𝐵 ( 𝑦 ≤ 𝑧 → 𝜑 ) → ( ∀ 𝑦 ∈ 𝑤 ∃ 𝑥 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 ( 𝑦 ≤ 𝑧 → 𝜑 ) → ( ∃ 𝑦 ∈ 𝑤 ∀ 𝑢 ∈ 𝑤 𝑢 ≤ 𝑦 → ∃ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( 𝑦 ≤ 𝑧 → ∀ 𝑥 ∈ 𝐴 𝜑 ) ) ) ) ) )
90 89 3impd ⊢ ( 𝐵 ⊆ ℝ → ( ( 𝑤 ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝑤 ∀ 𝑧 ∈ 𝐵 ( 𝑦 ≤ 𝑧 → 𝜑 ) ∧ ∀ 𝑦 ∈ 𝑤 ∃ 𝑥 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 ( 𝑦 ≤ 𝑧 → 𝜑 ) ) → ( ∃ 𝑦 ∈ 𝑤 ∀ 𝑢 ∈ 𝑤 𝑢 ≤ 𝑦 → ∃ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( 𝑦 ≤ 𝑧 → ∀ 𝑥 ∈ 𝐴 𝜑 ) ) ) )
91 90 3ad2ant3 ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐵 ⊆ ℝ ) → ( ( 𝑤 ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝑤 ∀ 𝑧 ∈ 𝐵 ( 𝑦 ≤ 𝑧 → 𝜑 ) ∧ ∀ 𝑦 ∈ 𝑤 ∃ 𝑥 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 ( 𝑦 ≤ 𝑧 → 𝜑 ) ) → ( ∃ 𝑦 ∈ 𝑤 ∀ 𝑢 ∈ 𝑤 𝑢 ≤ 𝑦 → ∃ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( 𝑦 ≤ 𝑧 → ∀ 𝑥 ∈ 𝐴 𝜑 ) ) ) )
92 91 adantr ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐵 ⊆ ℝ ) ∧ 𝑤 ∈ Fin ) → ( ( 𝑤 ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝑤 ∀ 𝑧 ∈ 𝐵 ( 𝑦 ≤ 𝑧 → 𝜑 ) ∧ ∀ 𝑦 ∈ 𝑤 ∃ 𝑥 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 ( 𝑦 ≤ 𝑧 → 𝜑 ) ) → ( ∃ 𝑦 ∈ 𝑤 ∀ 𝑢 ∈ 𝑤 𝑢 ≤ 𝑦 → ∃ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( 𝑦 ≤ 𝑧 → ∀ 𝑥 ∈ 𝐴 𝜑 ) ) ) )
93 26 92 mpdd ⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐵 ⊆ ℝ ) ∧ 𝑤 ∈ Fin ) → ( ( 𝑤 ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝑤 ∀ 𝑧 ∈ 𝐵 ( 𝑦 ≤ 𝑧 → 𝜑 ) ∧ ∀ 𝑦 ∈ 𝑤 ∃ 𝑥 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 ( 𝑦 ≤ 𝑧 → 𝜑 ) ) → ∃ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( 𝑦 ≤ 𝑧 → ∀ 𝑥 ∈ 𝐴 𝜑 ) ) )
94 93 rexlimdva ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐵 ⊆ ℝ ) → ( ∃ 𝑤 ∈ Fin ( 𝑤 ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝑤 ∀ 𝑧 ∈ 𝐵 ( 𝑦 ≤ 𝑧 → 𝜑 ) ∧ ∀ 𝑦 ∈ 𝑤 ∃ 𝑥 ∈ 𝐴 ∀ 𝑧 ∈ 𝐵 ( 𝑦 ≤ 𝑧 → 𝜑 ) ) → ∃ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( 𝑦 ≤ 𝑧 → ∀ 𝑥 ∈ 𝐴 𝜑 ) ) )
95 6 94 syld ⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐵 ⊆ ℝ ) → ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( 𝑦 ≤ 𝑧 → 𝜑 ) → ∃ 𝑦 ∈ 𝐵 ∀ 𝑧 ∈ 𝐵 ( 𝑦 ≤ 𝑧 → ∀ 𝑥 ∈ 𝐴 𝜑 ) ) )