Metamath Proof Explorer

Theorem noinfbnd1lem6

Description: Lemma for noinfbnd1 . Establish a hard lower bound when there is no minimum. (Contributed by Scott Fenton, 9-Aug-2024)

Ref Expression
Hypothesis noinfbnd1.1 ⊢ T = if ∃ x ∈ B ∀ y ∈ B ¬ y < s x ι x ∈ B | ∀ y ∈ B ¬ y < s x ∪ dom ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x 1 𝑜 g ∈ y | ∃ u ∈ B y ∈ dom ⁡ u ∧ ∀ v ∈ B ¬ u < s v → u ↾ suc ⁡ y = v ↾ suc ⁡ y ⟼ ι x | ∃ u ∈ B g ∈ dom ⁡ u ∧ ∀ v ∈ B ¬ u < s v → u ↾ suc ⁡ g = v ↾ suc ⁡ g ∧ u ⁡ g = x
Assertion noinfbnd1lem6 ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ U ∈ B → T < s U ↾ dom ⁡ T

Proof

Step Hyp Ref Expression
1 noinfbnd1.1 ⊢ T = if ∃ x ∈ B ∀ y ∈ B ¬ y < s x ι x ∈ B | ∀ y ∈ B ¬ y < s x ∪ dom ⁡ ι x ∈ B | ∀ y ∈ B ¬ y < s x 1 𝑜 g ∈ y | ∃ u ∈ B y ∈ dom ⁡ u ∧ ∀ v ∈ B ¬ u < s v → u ↾ suc ⁡ y = v ↾ suc ⁡ y ⟼ ι x | ∃ u ∈ B g ∈ dom ⁡ u ∧ ∀ v ∈ B ¬ u < s v → u ↾ suc ⁡ g = v ↾ suc ⁡ g ∧ u ⁡ g = x
2 simp2l ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ U ∈ B → B ⊆ No
3 simp3 ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ U ∈ B → U ∈ B
4 2 3 sseldd ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ U ∈ B → U ∈ No
5 nofv ⊢ U ∈ No → U ⁡ dom ⁡ T = ∅ ∨ U ⁡ dom ⁡ T = 1 𝑜 ∨ U ⁡ dom ⁡ T = 2 𝑜
6 4 5 syl ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ U ∈ B → U ⁡ dom ⁡ T = ∅ ∨ U ⁡ dom ⁡ T = 1 𝑜 ∨ U ⁡ dom ⁡ T = 2 𝑜
7 3oran ⊢ U ⁡ dom ⁡ T = ∅ ∨ U ⁡ dom ⁡ T = 1 𝑜 ∨ U ⁡ dom ⁡ T = 2 𝑜 ↔ ¬ ¬ U ⁡ dom ⁡ T = ∅ ∧ ¬ U ⁡ dom ⁡ T = 1 𝑜 ∧ ¬ U ⁡ dom ⁡ T = 2 𝑜
8 6 7 sylib ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ U ∈ B → ¬ ¬ U ⁡ dom ⁡ T = ∅ ∧ ¬ U ⁡ dom ⁡ T = 1 𝑜 ∧ ¬ U ⁡ dom ⁡ T = 2 𝑜
9 simpl1 ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ U ∈ B ∧ T = U ↾ dom ⁡ T → ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x
10 simpl2 ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ U ∈ B ∧ T = U ↾ dom ⁡ T → B ⊆ No ∧ B ∈ V
11 simpl3 ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ U ∈ B ∧ T = U ↾ dom ⁡ T → U ∈ B
12 simpr ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ U ∈ B ∧ T = U ↾ dom ⁡ T → T = U ↾ dom ⁡ T
13 12 eqcomd ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ U ∈ B ∧ T = U ↾ dom ⁡ T → U ↾ dom ⁡ T = T
14 1 noinfbnd1lem4 ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ U ∈ B ∧ U ↾ dom ⁡ T = T → U ⁡ dom ⁡ T ≠ ∅
15 9 10 11 13 14 syl112anc ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ U ∈ B ∧ T = U ↾ dom ⁡ T → U ⁡ dom ⁡ T ≠ ∅
16 15 neneqd ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ U ∈ B ∧ T = U ↾ dom ⁡ T → ¬ U ⁡ dom ⁡ T = ∅
17 1 noinfbnd1lem3 ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ U ∈ B ∧ U ↾ dom ⁡ T = T → U ⁡ dom ⁡ T ≠ 1 𝑜
18 9 10 11 13 17 syl112anc ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ U ∈ B ∧ T = U ↾ dom ⁡ T → U ⁡ dom ⁡ T ≠ 1 𝑜
19 18 neneqd ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ U ∈ B ∧ T = U ↾ dom ⁡ T → ¬ U ⁡ dom ⁡ T = 1 𝑜
20 1 noinfbnd1lem5 ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ U ∈ B ∧ U ↾ dom ⁡ T = T → U ⁡ dom ⁡ T ≠ 2 𝑜
21 9 10 11 13 20 syl112anc ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ U ∈ B ∧ T = U ↾ dom ⁡ T → U ⁡ dom ⁡ T ≠ 2 𝑜
22 21 neneqd ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ U ∈ B ∧ T = U ↾ dom ⁡ T → ¬ U ⁡ dom ⁡ T = 2 𝑜
23 16 19 22 3jca ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ U ∈ B ∧ T = U ↾ dom ⁡ T → ¬ U ⁡ dom ⁡ T = ∅ ∧ ¬ U ⁡ dom ⁡ T = 1 𝑜 ∧ ¬ U ⁡ dom ⁡ T = 2 𝑜
24 8 23 mtand ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ U ∈ B → ¬ T = U ↾ dom ⁡ T
25 1 noinfbnd1lem1 ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ U ∈ B → ¬ U ↾ dom ⁡ T < s T
26 1 noinfno ⊢ B ⊆ No ∧ B ∈ V → T ∈ No
27 26 3ad2ant2 ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ U ∈ B → T ∈ No
28 nodmon ⊢ T ∈ No → dom ⁡ T ∈ On
29 27 28 syl ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ U ∈ B → dom ⁡ T ∈ On
30 noreson ⊢ U ∈ No ∧ dom ⁡ T ∈ On → U ↾ dom ⁡ T ∈ No
31 4 29 30 syl2anc ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ U ∈ B → U ↾ dom ⁡ T ∈ No
32 ltsso ⊢ < s Or No
33 solin ⊢ < s Or No ∧ T ∈ No ∧ U ↾ dom ⁡ T ∈ No → T < s U ↾ dom ⁡ T ∨ T = U ↾ dom ⁡ T ∨ U ↾ dom ⁡ T < s T
34 32 33 mpan ⊢ T ∈ No ∧ U ↾ dom ⁡ T ∈ No → T < s U ↾ dom ⁡ T ∨ T = U ↾ dom ⁡ T ∨ U ↾ dom ⁡ T < s T
35 27 31 34 syl2anc ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ U ∈ B → T < s U ↾ dom ⁡ T ∨ T = U ↾ dom ⁡ T ∨ U ↾ dom ⁡ T < s T
36 24 25 35 ecase23d ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ U ∈ B → T < s U ↾ dom ⁡ T