Metamath Proof Explorer

Theorem noinfbnd1lem2

Description: Lemma for noinfbnd1 . When there is no minimum, if any member of B is a prolongment of T , then so are all elements below it. (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 noinfbnd1lem2 ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ U ∈ B ∧ U ↾ dom ⁡ T = T ∧ W ∈ B ∧ ¬ U < s W → W ↾ dom ⁡ T = 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 simp3rl ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ U ∈ B ∧ U ↾ dom ⁡ T = T ∧ W ∈ B ∧ ¬ U < s W → W ∈ B
3 1 noinfbnd1lem1 ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ W ∈ B → ¬ W ↾ dom ⁡ T < s T
4 2 3 syld3an3 ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ U ∈ B ∧ U ↾ dom ⁡ T = T ∧ W ∈ B ∧ ¬ U < s W → ¬ W ↾ dom ⁡ T < s T
5 simp3rr ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ U ∈ B ∧ U ↾ dom ⁡ T = T ∧ W ∈ B ∧ ¬ U < s W → ¬ U < s W
6 simp2l ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ U ∈ B ∧ U ↾ dom ⁡ T = T ∧ W ∈ B ∧ ¬ U < s W → B ⊆ No
7 simp3ll ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ U ∈ B ∧ U ↾ dom ⁡ T = T ∧ W ∈ B ∧ ¬ U < s W → U ∈ B
8 6 7 sseldd ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ U ∈ B ∧ U ↾ dom ⁡ T = T ∧ W ∈ B ∧ ¬ U < s W → U ∈ No
9 6 2 sseldd ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ U ∈ B ∧ U ↾ dom ⁡ T = T ∧ W ∈ B ∧ ¬ U < s W → W ∈ No
10 1 noinfno ⊢ B ⊆ No ∧ B ∈ V → T ∈ No
11 10 3ad2ant2 ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ U ∈ B ∧ U ↾ dom ⁡ T = T ∧ W ∈ B ∧ ¬ U < s W → T ∈ No
12 nodmon ⊢ T ∈ No → dom ⁡ T ∈ On
13 11 12 syl ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ U ∈ B ∧ U ↾ dom ⁡ T = T ∧ W ∈ B ∧ ¬ U < s W → dom ⁡ T ∈ On
14 ltsres ⊢ U ∈ No ∧ W ∈ No ∧ dom ⁡ T ∈ On → U ↾ dom ⁡ T < s W ↾ dom ⁡ T → U < s W
15 8 9 13 14 syl3anc ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ U ∈ B ∧ U ↾ dom ⁡ T = T ∧ W ∈ B ∧ ¬ U < s W → U ↾ dom ⁡ T < s W ↾ dom ⁡ T → U < s W
16 5 15 mtod ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ U ∈ B ∧ U ↾ dom ⁡ T = T ∧ W ∈ B ∧ ¬ U < s W → ¬ U ↾ dom ⁡ T < s W ↾ dom ⁡ T
17 simp3lr ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ U ∈ B ∧ U ↾ dom ⁡ T = T ∧ W ∈ B ∧ ¬ U < s W → U ↾ dom ⁡ T = T
18 17 breq1d ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ U ∈ B ∧ U ↾ dom ⁡ T = T ∧ W ∈ B ∧ ¬ U < s W → U ↾ dom ⁡ T < s W ↾ dom ⁡ T ↔ T < s W ↾ dom ⁡ T
19 16 18 mtbid ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ U ∈ B ∧ U ↾ dom ⁡ T = T ∧ W ∈ B ∧ ¬ U < s W → ¬ T < s W ↾ dom ⁡ T
20 noreson ⊢ W ∈ No ∧ dom ⁡ T ∈ On → W ↾ dom ⁡ T ∈ No
21 9 13 20 syl2anc ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ U ∈ B ∧ U ↾ dom ⁡ T = T ∧ W ∈ B ∧ ¬ U < s W → W ↾ dom ⁡ T ∈ No
22 ltsso ⊢ < s Or No
23 sotrieq2 ⊢ < s Or No ∧ W ↾ dom ⁡ T ∈ No ∧ T ∈ No → W ↾ dom ⁡ T = T ↔ ¬ W ↾ dom ⁡ T < s T ∧ ¬ T < s W ↾ dom ⁡ T
24 22 23 mpan ⊢ W ↾ dom ⁡ T ∈ No ∧ T ∈ No → W ↾ dom ⁡ T = T ↔ ¬ W ↾ dom ⁡ T < s T ∧ ¬ T < s W ↾ dom ⁡ T
25 21 11 24 syl2anc ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ U ∈ B ∧ U ↾ dom ⁡ T = T ∧ W ∈ B ∧ ¬ U < s W → W ↾ dom ⁡ T = T ↔ ¬ W ↾ dom ⁡ T < s T ∧ ¬ T < s W ↾ dom ⁡ T
26 4 19 25 mpbir2and ⊢ ¬ ∃ x ∈ B ∀ y ∈ B ¬ y < s x ∧ B ⊆ No ∧ B ∈ V ∧ U ∈ B ∧ U ↾ dom ⁡ T = T ∧ W ∈ B ∧ ¬ U < s W → W ↾ dom ⁡ T = T