Users' Mathboxes Mathbox for Jeff Madsen < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  filbcmb Structured version   Visualization version   GIF version

Theorem filbcmb 32595
Description: Combine a finite set of lower bounds. (Contributed by Jeff Madsen, 2-Sep-2009.)
Assertion
Ref Expression
filbcmb ((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐵 ⊆ ℝ) → (∀𝑥𝐴𝑦𝐵𝑧𝐵 (𝑦𝑧𝜑) → ∃𝑦𝐵𝑧𝐵 (𝑦𝑧 → ∀𝑥𝐴 𝜑)))
Distinct variable groups:   𝑥,𝐴,𝑦,𝑧   𝑥,𝐵,𝑦,𝑧   𝜑,𝑦
Allowed substitution hints:   𝜑(𝑥,𝑧)

Proof of Theorem filbcmb
Dummy variables 𝑢 𝑣 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 reex 9782 . . . . 5 ℝ ∈ V
21ssex 4629 . . . 4 (𝐵 ⊆ ℝ → 𝐵 ∈ V)
3 indexfi 8033 . . . . 5 ((𝐴 ∈ Fin ∧ 𝐵 ∈ V ∧ ∀𝑥𝐴𝑦𝐵𝑧𝐵 (𝑦𝑧𝜑)) → ∃𝑤 ∈ Fin (𝑤𝐵 ∧ ∀𝑥𝐴𝑦𝑤𝑧𝐵 (𝑦𝑧𝜑) ∧ ∀𝑦𝑤𝑥𝐴𝑧𝐵 (𝑦𝑧𝜑)))
433expia 1258 . . . 4 ((𝐴 ∈ Fin ∧ 𝐵 ∈ V) → (∀𝑥𝐴𝑦𝐵𝑧𝐵 (𝑦𝑧𝜑) → ∃𝑤 ∈ Fin (𝑤𝐵 ∧ ∀𝑥𝐴𝑦𝑤𝑧𝐵 (𝑦𝑧𝜑) ∧ ∀𝑦𝑤𝑥𝐴𝑧𝐵 (𝑦𝑧𝜑))))
52, 4sylan2 489 . . 3 ((𝐴 ∈ Fin ∧ 𝐵 ⊆ ℝ) → (∀𝑥𝐴𝑦𝐵𝑧𝐵 (𝑦𝑧𝜑) → ∃𝑤 ∈ Fin (𝑤𝐵 ∧ ∀𝑥𝐴𝑦𝑤𝑧𝐵 (𝑦𝑧𝜑) ∧ ∀𝑦𝑤𝑥𝐴𝑧𝐵 (𝑦𝑧𝜑))))
653adant2 1072 . 2 ((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐵 ⊆ ℝ) → (∀𝑥𝐴𝑦𝐵𝑧𝐵 (𝑦𝑧𝜑) → ∃𝑤 ∈ Fin (𝑤𝐵 ∧ ∀𝑥𝐴𝑦𝑤𝑧𝐵 (𝑦𝑧𝜑) ∧ ∀𝑦𝑤𝑥𝐴𝑧𝐵 (𝑦𝑧𝜑))))
7 r19.2z 3915 . . . . . . . . . . . 12 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴𝑦𝑤𝑧𝐵 (𝑦𝑧𝜑)) → ∃𝑥𝐴𝑦𝑤𝑧𝐵 (𝑦𝑧𝜑))
8 rexn0 3929 . . . . . . . . . . . . 13 (∃𝑦𝑤𝑧𝐵 (𝑦𝑧𝜑) → 𝑤 ≠ ∅)
98rexlimivw 2915 . . . . . . . . . . . 12 (∃𝑥𝐴𝑦𝑤𝑧𝐵 (𝑦𝑧𝜑) → 𝑤 ≠ ∅)
107, 9syl 17 . . . . . . . . . . 11 ((𝐴 ≠ ∅ ∧ ∀𝑥𝐴𝑦𝑤𝑧𝐵 (𝑦𝑧𝜑)) → 𝑤 ≠ ∅)
1110ex 448 . . . . . . . . . 10 (𝐴 ≠ ∅ → (∀𝑥𝐴𝑦𝑤𝑧𝐵 (𝑦𝑧𝜑) → 𝑤 ≠ ∅))
12113ad2ant2 1075 . . . . . . . . 9 ((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐵 ⊆ ℝ) → (∀𝑥𝐴𝑦𝑤𝑧𝐵 (𝑦𝑧𝜑) → 𝑤 ≠ ∅))
1312ad2antrr 757 . . . . . . . 8 ((((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐵 ⊆ ℝ) ∧ 𝑤 ∈ Fin) ∧ 𝑤𝐵) → (∀𝑥𝐴𝑦𝑤𝑧𝐵 (𝑦𝑧𝜑) → 𝑤 ≠ ∅))
14 sstr 3480 . . . . . . . . . . . . . 14 ((𝑤𝐵𝐵 ⊆ ℝ) → 𝑤 ⊆ ℝ)
1514ancoms 467 . . . . . . . . . . . . 13 ((𝐵 ⊆ ℝ ∧ 𝑤𝐵) → 𝑤 ⊆ ℝ)
16 fimaxre 10718 . . . . . . . . . . . . . 14 ((𝑤 ⊆ ℝ ∧ 𝑤 ∈ Fin ∧ 𝑤 ≠ ∅) → ∃𝑦𝑤𝑢𝑤 𝑢𝑦)
17163expia 1258 . . . . . . . . . . . . 13 ((𝑤 ⊆ ℝ ∧ 𝑤 ∈ Fin) → (𝑤 ≠ ∅ → ∃𝑦𝑤𝑢𝑤 𝑢𝑦))
1815, 17sylan 486 . . . . . . . . . . . 12 (((𝐵 ⊆ ℝ ∧ 𝑤𝐵) ∧ 𝑤 ∈ Fin) → (𝑤 ≠ ∅ → ∃𝑦𝑤𝑢𝑤 𝑢𝑦))
1918anasss 676 . . . . . . . . . . 11 ((𝐵 ⊆ ℝ ∧ (𝑤𝐵𝑤 ∈ Fin)) → (𝑤 ≠ ∅ → ∃𝑦𝑤𝑢𝑤 𝑢𝑦))
2019ancom2s 839 . . . . . . . . . 10 ((𝐵 ⊆ ℝ ∧ (𝑤 ∈ Fin ∧ 𝑤𝐵)) → (𝑤 ≠ ∅ → ∃𝑦𝑤𝑢𝑤 𝑢𝑦))
21203ad2antl3 1217 . . . . . . . . 9 (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐵 ⊆ ℝ) ∧ (𝑤 ∈ Fin ∧ 𝑤𝐵)) → (𝑤 ≠ ∅ → ∃𝑦𝑤𝑢𝑤 𝑢𝑦))
2221anassrs 677 . . . . . . . 8 ((((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐵 ⊆ ℝ) ∧ 𝑤 ∈ Fin) ∧ 𝑤𝐵) → (𝑤 ≠ ∅ → ∃𝑦𝑤𝑢𝑤 𝑢𝑦))
2313, 22syld 45 . . . . . . 7 ((((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐵 ⊆ ℝ) ∧ 𝑤 ∈ Fin) ∧ 𝑤𝐵) → (∀𝑥𝐴𝑦𝑤𝑧𝐵 (𝑦𝑧𝜑) → ∃𝑦𝑤𝑢𝑤 𝑢𝑦))
2423a1dd 47 . . . . . 6 ((((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐵 ⊆ ℝ) ∧ 𝑤 ∈ Fin) ∧ 𝑤𝐵) → (∀𝑥𝐴𝑦𝑤𝑧𝐵 (𝑦𝑧𝜑) → (∀𝑦𝑤𝑥𝐴𝑧𝐵 (𝑦𝑧𝜑) → ∃𝑦𝑤𝑢𝑤 𝑢𝑦)))
2524ex 448 . . . . 5 (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐵 ⊆ ℝ) ∧ 𝑤 ∈ Fin) → (𝑤𝐵 → (∀𝑥𝐴𝑦𝑤𝑧𝐵 (𝑦𝑧𝜑) → (∀𝑦𝑤𝑥𝐴𝑧𝐵 (𝑦𝑧𝜑) → ∃𝑦𝑤𝑢𝑤 𝑢𝑦))))
26253impd 1272 . . . 4 (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐵 ⊆ ℝ) ∧ 𝑤 ∈ Fin) → ((𝑤𝐵 ∧ ∀𝑥𝐴𝑦𝑤𝑧𝐵 (𝑦𝑧𝜑) ∧ ∀𝑦𝑤𝑥𝐴𝑧𝐵 (𝑦𝑧𝜑)) → ∃𝑦𝑤𝑢𝑤 𝑢𝑦))
27 nfv 1796 . . . . . . . . . . . 12 𝑦(𝐵 ⊆ ℝ ∧ 𝑤𝐵)
28 nfcv 2655 . . . . . . . . . . . . 13 𝑦𝐴
29 nfre1 2892 . . . . . . . . . . . . 13 𝑦𝑦𝑤𝑧𝐵 (𝑦𝑧𝜑)
3028, 29nfral 2833 . . . . . . . . . . . 12 𝑦𝑥𝐴𝑦𝑤𝑧𝐵 (𝑦𝑧𝜑)
3127, 30nfan 2059 . . . . . . . . . . 11 𝑦((𝐵 ⊆ ℝ ∧ 𝑤𝐵) ∧ ∀𝑥𝐴𝑦𝑤𝑧𝐵 (𝑦𝑧𝜑))
32 nfv 1796 . . . . . . . . . . . . . . 15 𝑧(𝐵 ⊆ ℝ ∧ 𝑤𝐵)
33 nfcv 2655 . . . . . . . . . . . . . . . 16 𝑧𝐴
34 nfcv 2655 . . . . . . . . . . . . . . . . 17 𝑧𝑤
35 nfra1 2829 . . . . . . . . . . . . . . . . 17 𝑧𝑧𝐵 (𝑦𝑧𝜑)
3634, 35nfrex 2894 . . . . . . . . . . . . . . . 16 𝑧𝑦𝑤𝑧𝐵 (𝑦𝑧𝜑)
3733, 36nfral 2833 . . . . . . . . . . . . . . 15 𝑧𝑥𝐴𝑦𝑤𝑧𝐵 (𝑦𝑧𝜑)
3832, 37nfan 2059 . . . . . . . . . . . . . 14 𝑧((𝐵 ⊆ ℝ ∧ 𝑤𝐵) ∧ ∀𝑥𝐴𝑦𝑤𝑧𝐵 (𝑦𝑧𝜑))
39 nfv 1796 . . . . . . . . . . . . . 14 𝑧(𝑦𝑤 ∧ ∀𝑢𝑤 𝑢𝑦)
4038, 39nfan 2059 . . . . . . . . . . . . 13 𝑧(((𝐵 ⊆ ℝ ∧ 𝑤𝐵) ∧ ∀𝑥𝐴𝑦𝑤𝑧𝐵 (𝑦𝑧𝜑)) ∧ (𝑦𝑤 ∧ ∀𝑢𝑤 𝑢𝑦))
41 breq1 4484 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 = 𝑣 → (𝑦𝑧𝑣𝑧))
4241imbi1d 329 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = 𝑣 → ((𝑦𝑧𝜑) ↔ (𝑣𝑧𝜑)))
4342ralbidv 2873 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 𝑣 → (∀𝑧𝐵 (𝑦𝑧𝜑) ↔ ∀𝑧𝐵 (𝑣𝑧𝜑)))
4443cbvrexv 3052 . . . . . . . . . . . . . . . . . . 19 (∃𝑦𝑤𝑧𝐵 (𝑦𝑧𝜑) ↔ ∃𝑣𝑤𝑧𝐵 (𝑣𝑧𝜑))
45 rsp 2817 . . . . . . . . . . . . . . . . . . . . . 22 (∀𝑧𝐵 (𝑣𝑧𝜑) → (𝑧𝐵 → (𝑣𝑧𝜑)))
46 ssel2 3467 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑤𝐵𝑣𝑤) → 𝑣𝐵)
47 ssel2 3467 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝐵 ⊆ ℝ ∧ 𝑣𝐵) → 𝑣 ∈ ℝ)
4846, 47sylan2 489 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐵 ⊆ ℝ ∧ (𝑤𝐵𝑣𝑤)) → 𝑣 ∈ ℝ)
4948anassrs 677 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝐵 ⊆ ℝ ∧ 𝑤𝐵) ∧ 𝑣𝑤) → 𝑣 ∈ ℝ)
5049adantlr 746 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐵 ⊆ ℝ ∧ 𝑤𝐵) ∧ (𝑦𝑤 ∧ ∀𝑢𝑤 𝑢𝑦)) ∧ 𝑣𝑤) → 𝑣 ∈ ℝ)
5150adantlr 746 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝐵 ⊆ ℝ ∧ 𝑤𝐵) ∧ (𝑦𝑤 ∧ ∀𝑢𝑤 𝑢𝑦)) ∧ (𝑧𝐵𝑦𝑧)) ∧ 𝑣𝑤) → 𝑣 ∈ ℝ)
52 ssel2 3467 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑤𝐵𝑦𝑤) → 𝑦𝐵)
53 ssel2 3467 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝐵 ⊆ ℝ ∧ 𝑦𝐵) → 𝑦 ∈ ℝ)
5452, 53sylan2 489 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐵 ⊆ ℝ ∧ (𝑤𝐵𝑦𝑤)) → 𝑦 ∈ ℝ)
5554anassrs 677 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝐵 ⊆ ℝ ∧ 𝑤𝐵) ∧ 𝑦𝑤) → 𝑦 ∈ ℝ)
5655adantrr 748 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝐵 ⊆ ℝ ∧ 𝑤𝐵) ∧ (𝑦𝑤 ∧ ∀𝑢𝑤 𝑢𝑦)) → 𝑦 ∈ ℝ)
5756ad2antrr 757 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝐵 ⊆ ℝ ∧ 𝑤𝐵) ∧ (𝑦𝑤 ∧ ∀𝑢𝑤 𝑢𝑦)) ∧ (𝑧𝐵𝑦𝑧)) ∧ 𝑣𝑤) → 𝑦 ∈ ℝ)
58 ssel2 3467 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐵 ⊆ ℝ ∧ 𝑧𝐵) → 𝑧 ∈ ℝ)
5958adantlr 746 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝐵 ⊆ ℝ ∧ 𝑤𝐵) ∧ 𝑧𝐵) → 𝑧 ∈ ℝ)
6059ad2ant2r 778 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐵 ⊆ ℝ ∧ 𝑤𝐵) ∧ (𝑦𝑤 ∧ ∀𝑢𝑤 𝑢𝑦)) ∧ (𝑧𝐵𝑦𝑧)) → 𝑧 ∈ ℝ)
6160adantr 479 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝐵 ⊆ ℝ ∧ 𝑤𝐵) ∧ (𝑦𝑤 ∧ ∀𝑢𝑤 𝑢𝑦)) ∧ (𝑧𝐵𝑦𝑧)) ∧ 𝑣𝑤) → 𝑧 ∈ ℝ)
62 breq1 4484 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑢 = 𝑣 → (𝑢𝑦𝑣𝑦))
6362rspccva 3185 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((∀𝑢𝑤 𝑢𝑦𝑣𝑤) → 𝑣𝑦)
6463adantll 745 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑦𝑤 ∧ ∀𝑢𝑤 𝑢𝑦) ∧ 𝑣𝑤) → 𝑣𝑦)
6564adantll 745 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐵 ⊆ ℝ ∧ 𝑤𝐵) ∧ (𝑦𝑤 ∧ ∀𝑢𝑤 𝑢𝑦)) ∧ 𝑣𝑤) → 𝑣𝑦)
6665adantlr 746 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝐵 ⊆ ℝ ∧ 𝑤𝐵) ∧ (𝑦𝑤 ∧ ∀𝑢𝑤 𝑢𝑦)) ∧ (𝑧𝐵𝑦𝑧)) ∧ 𝑣𝑤) → 𝑣𝑦)
67 simplrr 796 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝐵 ⊆ ℝ ∧ 𝑤𝐵) ∧ (𝑦𝑤 ∧ ∀𝑢𝑤 𝑢𝑦)) ∧ (𝑧𝐵𝑦𝑧)) ∧ 𝑣𝑤) → 𝑦𝑧)
6851, 57, 61, 66, 67letrd 9945 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝐵 ⊆ ℝ ∧ 𝑤𝐵) ∧ (𝑦𝑤 ∧ ∀𝑢𝑤 𝑢𝑦)) ∧ (𝑧𝐵𝑦𝑧)) ∧ 𝑣𝑤) → 𝑣𝑧)
69 pm2.27 40 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑧𝐵 → ((𝑧𝐵 → (𝑣𝑧𝜑)) → (𝑣𝑧𝜑)))
7069adantr 479 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑧𝐵𝑦𝑧) → ((𝑧𝐵 → (𝑣𝑧𝜑)) → (𝑣𝑧𝜑)))
7170ad2antlr 758 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝐵 ⊆ ℝ ∧ 𝑤𝐵) ∧ (𝑦𝑤 ∧ ∀𝑢𝑤 𝑢𝑦)) ∧ (𝑧𝐵𝑦𝑧)) ∧ 𝑣𝑤) → ((𝑧𝐵 → (𝑣𝑧𝜑)) → (𝑣𝑧𝜑)))
7268, 71mpid 42 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝐵 ⊆ ℝ ∧ 𝑤𝐵) ∧ (𝑦𝑤 ∧ ∀𝑢𝑤 𝑢𝑦)) ∧ (𝑧𝐵𝑦𝑧)) ∧ 𝑣𝑤) → ((𝑧𝐵 → (𝑣𝑧𝜑)) → 𝜑))
7345, 72syl5 33 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐵 ⊆ ℝ ∧ 𝑤𝐵) ∧ (𝑦𝑤 ∧ ∀𝑢𝑤 𝑢𝑦)) ∧ (𝑧𝐵𝑦𝑧)) ∧ 𝑣𝑤) → (∀𝑧𝐵 (𝑣𝑧𝜑) → 𝜑))
7473adantlr 746 . . . . . . . . . . . . . . . . . . . 20 ((((((𝐵 ⊆ ℝ ∧ 𝑤𝐵) ∧ (𝑦𝑤 ∧ ∀𝑢𝑤 𝑢𝑦)) ∧ (𝑧𝐵𝑦𝑧)) ∧ 𝑥𝐴) ∧ 𝑣𝑤) → (∀𝑧𝐵 (𝑣𝑧𝜑) → 𝜑))
7574rexlimdva 2917 . . . . . . . . . . . . . . . . . . 19 (((((𝐵 ⊆ ℝ ∧ 𝑤𝐵) ∧ (𝑦𝑤 ∧ ∀𝑢𝑤 𝑢𝑦)) ∧ (𝑧𝐵𝑦𝑧)) ∧ 𝑥𝐴) → (∃𝑣𝑤𝑧𝐵 (𝑣𝑧𝜑) → 𝜑))
7644, 75syl5bi 230 . . . . . . . . . . . . . . . . . 18 (((((𝐵 ⊆ ℝ ∧ 𝑤𝐵) ∧ (𝑦𝑤 ∧ ∀𝑢𝑤 𝑢𝑦)) ∧ (𝑧𝐵𝑦𝑧)) ∧ 𝑥𝐴) → (∃𝑦𝑤𝑧𝐵 (𝑦𝑧𝜑) → 𝜑))
7776ralimdva 2849 . . . . . . . . . . . . . . . . 17 ((((𝐵 ⊆ ℝ ∧ 𝑤𝐵) ∧ (𝑦𝑤 ∧ ∀𝑢𝑤 𝑢𝑦)) ∧ (𝑧𝐵𝑦𝑧)) → (∀𝑥𝐴𝑦𝑤𝑧𝐵 (𝑦𝑧𝜑) → ∀𝑥𝐴 𝜑))
7877imp 443 . . . . . . . . . . . . . . . 16 (((((𝐵 ⊆ ℝ ∧ 𝑤𝐵) ∧ (𝑦𝑤 ∧ ∀𝑢𝑤 𝑢𝑦)) ∧ (𝑧𝐵𝑦𝑧)) ∧ ∀𝑥𝐴𝑦𝑤𝑧𝐵 (𝑦𝑧𝜑)) → ∀𝑥𝐴 𝜑)
7978an32s 841 . . . . . . . . . . . . . . 15 (((((𝐵 ⊆ ℝ ∧ 𝑤𝐵) ∧ (𝑦𝑤 ∧ ∀𝑢𝑤 𝑢𝑦)) ∧ ∀𝑥𝐴𝑦𝑤𝑧𝐵 (𝑦𝑧𝜑)) ∧ (𝑧𝐵𝑦𝑧)) → ∀𝑥𝐴 𝜑)
8079exp32 628 . . . . . . . . . . . . . 14 ((((𝐵 ⊆ ℝ ∧ 𝑤𝐵) ∧ (𝑦𝑤 ∧ ∀𝑢𝑤 𝑢𝑦)) ∧ ∀𝑥𝐴𝑦𝑤𝑧𝐵 (𝑦𝑧𝜑)) → (𝑧𝐵 → (𝑦𝑧 → ∀𝑥𝐴 𝜑)))
8180an32s 841 . . . . . . . . . . . . 13 ((((𝐵 ⊆ ℝ ∧ 𝑤𝐵) ∧ ∀𝑥𝐴𝑦𝑤𝑧𝐵 (𝑦𝑧𝜑)) ∧ (𝑦𝑤 ∧ ∀𝑢𝑤 𝑢𝑦)) → (𝑧𝐵 → (𝑦𝑧 → ∀𝑥𝐴 𝜑)))
8240, 81ralrimi 2844 . . . . . . . . . . . 12 ((((𝐵 ⊆ ℝ ∧ 𝑤𝐵) ∧ ∀𝑥𝐴𝑦𝑤𝑧𝐵 (𝑦𝑧𝜑)) ∧ (𝑦𝑤 ∧ ∀𝑢𝑤 𝑢𝑦)) → ∀𝑧𝐵 (𝑦𝑧 → ∀𝑥𝐴 𝜑))
8382exp32 628 . . . . . . . . . . 11 (((𝐵 ⊆ ℝ ∧ 𝑤𝐵) ∧ ∀𝑥𝐴𝑦𝑤𝑧𝐵 (𝑦𝑧𝜑)) → (𝑦𝑤 → (∀𝑢𝑤 𝑢𝑦 → ∀𝑧𝐵 (𝑦𝑧 → ∀𝑥𝐴 𝜑))))
8431, 83reximdai 2899 . . . . . . . . . 10 (((𝐵 ⊆ ℝ ∧ 𝑤𝐵) ∧ ∀𝑥𝐴𝑦𝑤𝑧𝐵 (𝑦𝑧𝜑)) → (∃𝑦𝑤𝑢𝑤 𝑢𝑦 → ∃𝑦𝑤𝑧𝐵 (𝑦𝑧 → ∀𝑥𝐴 𝜑)))
8584adantrr 748 . . . . . . . . 9 (((𝐵 ⊆ ℝ ∧ 𝑤𝐵) ∧ (∀𝑥𝐴𝑦𝑤𝑧𝐵 (𝑦𝑧𝜑) ∧ ∀𝑦𝑤𝑥𝐴𝑧𝐵 (𝑦𝑧𝜑))) → (∃𝑦𝑤𝑢𝑤 𝑢𝑦 → ∃𝑦𝑤𝑧𝐵 (𝑦𝑧 → ∀𝑥𝐴 𝜑)))
86 ssrexv 3534 . . . . . . . . . 10 (𝑤𝐵 → (∃𝑦𝑤𝑧𝐵 (𝑦𝑧 → ∀𝑥𝐴 𝜑) → ∃𝑦𝐵𝑧𝐵 (𝑦𝑧 → ∀𝑥𝐴 𝜑)))
8786ad2antlr 758 . . . . . . . . 9 (((𝐵 ⊆ ℝ ∧ 𝑤𝐵) ∧ (∀𝑥𝐴𝑦𝑤𝑧𝐵 (𝑦𝑧𝜑) ∧ ∀𝑦𝑤𝑥𝐴𝑧𝐵 (𝑦𝑧𝜑))) → (∃𝑦𝑤𝑧𝐵 (𝑦𝑧 → ∀𝑥𝐴 𝜑) → ∃𝑦𝐵𝑧𝐵 (𝑦𝑧 → ∀𝑥𝐴 𝜑)))
8885, 87syld 45 . . . . . . . 8 (((𝐵 ⊆ ℝ ∧ 𝑤𝐵) ∧ (∀𝑥𝐴𝑦𝑤𝑧𝐵 (𝑦𝑧𝜑) ∧ ∀𝑦𝑤𝑥𝐴𝑧𝐵 (𝑦𝑧𝜑))) → (∃𝑦𝑤𝑢𝑤 𝑢𝑦 → ∃𝑦𝐵𝑧𝐵 (𝑦𝑧 → ∀𝑥𝐴 𝜑)))
8988exp43 637 . . . . . . 7 (𝐵 ⊆ ℝ → (𝑤𝐵 → (∀𝑥𝐴𝑦𝑤𝑧𝐵 (𝑦𝑧𝜑) → (∀𝑦𝑤𝑥𝐴𝑧𝐵 (𝑦𝑧𝜑) → (∃𝑦𝑤𝑢𝑤 𝑢𝑦 → ∃𝑦𝐵𝑧𝐵 (𝑦𝑧 → ∀𝑥𝐴 𝜑))))))
90893impd 1272 . . . . . 6 (𝐵 ⊆ ℝ → ((𝑤𝐵 ∧ ∀𝑥𝐴𝑦𝑤𝑧𝐵 (𝑦𝑧𝜑) ∧ ∀𝑦𝑤𝑥𝐴𝑧𝐵 (𝑦𝑧𝜑)) → (∃𝑦𝑤𝑢𝑤 𝑢𝑦 → ∃𝑦𝐵𝑧𝐵 (𝑦𝑧 → ∀𝑥𝐴 𝜑))))
91903ad2ant3 1076 . . . . 5 ((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐵 ⊆ ℝ) → ((𝑤𝐵 ∧ ∀𝑥𝐴𝑦𝑤𝑧𝐵 (𝑦𝑧𝜑) ∧ ∀𝑦𝑤𝑥𝐴𝑧𝐵 (𝑦𝑧𝜑)) → (∃𝑦𝑤𝑢𝑤 𝑢𝑦 → ∃𝑦𝐵𝑧𝐵 (𝑦𝑧 → ∀𝑥𝐴 𝜑))))
9291adantr 479 . . . 4 (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐵 ⊆ ℝ) ∧ 𝑤 ∈ Fin) → ((𝑤𝐵 ∧ ∀𝑥𝐴𝑦𝑤𝑧𝐵 (𝑦𝑧𝜑) ∧ ∀𝑦𝑤𝑥𝐴𝑧𝐵 (𝑦𝑧𝜑)) → (∃𝑦𝑤𝑢𝑤 𝑢𝑦 → ∃𝑦𝐵𝑧𝐵 (𝑦𝑧 → ∀𝑥𝐴 𝜑))))
9326, 92mpdd 41 . . 3 (((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐵 ⊆ ℝ) ∧ 𝑤 ∈ Fin) → ((𝑤𝐵 ∧ ∀𝑥𝐴𝑦𝑤𝑧𝐵 (𝑦𝑧𝜑) ∧ ∀𝑦𝑤𝑥𝐴𝑧𝐵 (𝑦𝑧𝜑)) → ∃𝑦𝐵𝑧𝐵 (𝑦𝑧 → ∀𝑥𝐴 𝜑)))
9493rexlimdva 2917 . 2 ((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐵 ⊆ ℝ) → (∃𝑤 ∈ Fin (𝑤𝐵 ∧ ∀𝑥𝐴𝑦𝑤𝑧𝐵 (𝑦𝑧𝜑) ∧ ∀𝑦𝑤𝑥𝐴𝑧𝐵 (𝑦𝑧𝜑)) → ∃𝑦𝐵𝑧𝐵 (𝑦𝑧 → ∀𝑥𝐴 𝜑)))
956, 94syld 45 1 ((𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ 𝐵 ⊆ ℝ) → (∀𝑥𝐴𝑦𝐵𝑧𝐵 (𝑦𝑧𝜑) → ∃𝑦𝐵𝑧𝐵 (𝑦𝑧 → ∀𝑥𝐴 𝜑)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  w3a 1030  wcel 1938  wne 2684  wral 2800  wrex 2801  Vcvv 3077  wss 3444  c0 3777   class class class wbr 4481  Fincfn 7717  cr 9690  cle 9830
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1700  ax-4 1713  ax-5 1793  ax-6 1838  ax-7 1885  ax-8 1940  ax-9 1947  ax-10 1966  ax-11 1971  ax-12 1983  ax-13 2137  ax-ext 2494  ax-sep 4607  ax-nul 4616  ax-pow 4668  ax-pr 4732  ax-un 6723  ax-cnex 9747  ax-resscn 9748  ax-pre-lttri 9765  ax-pre-lttrn 9766
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1699  df-sb 1831  df-eu 2366  df-mo 2367  df-clab 2501  df-cleq 2507  df-clel 2510  df-nfc 2644  df-ne 2686  df-nel 2687  df-ral 2805  df-rex 2806  df-reu 2807  df-rab 2809  df-v 3079  df-sbc 3307  df-csb 3404  df-dif 3447  df-un 3449  df-in 3451  df-ss 3458  df-pss 3460  df-nul 3778  df-if 3940  df-pw 4013  df-sn 4029  df-pr 4031  df-tp 4033  df-op 4035  df-uni 4271  df-br 4482  df-opab 4542  df-mpt 4543  df-tr 4579  df-eprel 4843  df-id 4847  df-po 4853  df-so 4854  df-fr 4891  df-we 4893  df-xp 4938  df-rel 4939  df-cnv 4940  df-co 4941  df-dm 4942  df-rn 4943  df-res 4944  df-ima 4945  df-ord 5533  df-on 5534  df-lim 5535  df-suc 5536  df-iota 5653  df-fun 5691  df-fn 5692  df-f 5693  df-f1 5694  df-fo 5695  df-f1o 5696  df-fv 5697  df-om 6834  df-1o 7323  df-er 7505  df-en 7718  df-dom 7719  df-sdom 7720  df-fin 7721  df-pnf 9831  df-mnf 9832  df-xr 9833  df-ltxr 9834  df-le 9835
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator