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 ⊢ 𝑇 = if ( ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 , ( ( ℩ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ) ∪ { ⟨ dom ( ℩ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ) , 1o ⟩ } ) , ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢 ∈ 𝐵 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥 ∃ 𝑢 ∈ 𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢 ‘ 𝑔 ) = 𝑥 ) ) ) )
Assertion noinfbnd1lem6 ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ 𝑈 ∈ 𝐵 ) → 𝑇 <s ( 𝑈 ↾ dom 𝑇 ) )

Proof

Step Hyp Ref Expression
1 noinfbnd1.1 ⊢ 𝑇 = if ( ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 , ( ( ℩ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ) ∪ { ⟨ dom ( ℩ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ) , 1o ⟩ } ) , ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢 ∈ 𝐵 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥 ∃ 𝑢 ∈ 𝐵 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐵 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢 ‘ 𝑔 ) = 𝑥 ) ) ) )
2 simp2l ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ 𝑈 ∈ 𝐵 ) → 𝐵 ⊆ No )
3 simp3 ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ 𝑈 ∈ 𝐵 ) → 𝑈 ∈ 𝐵 )
4 2 3 sseldd ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ 𝑈 ∈ 𝐵 ) → 𝑈 ∈ No )
5 nofv ⊢ ( 𝑈 ∈ No → ( ( 𝑈 ‘ dom 𝑇 ) = ∅ ∨ ( 𝑈 ‘ dom 𝑇 ) = 1o ∨ ( 𝑈 ‘ dom 𝑇 ) = 2o ) )
6 4 5 syl ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ 𝑈 ∈ 𝐵 ) → ( ( 𝑈 ‘ dom 𝑇 ) = ∅ ∨ ( 𝑈 ‘ dom 𝑇 ) = 1o ∨ ( 𝑈 ‘ dom 𝑇 ) = 2o ) )
7 3oran ⊢ ( ( ( 𝑈 ‘ dom 𝑇 ) = ∅ ∨ ( 𝑈 ‘ dom 𝑇 ) = 1o ∨ ( 𝑈 ‘ dom 𝑇 ) = 2o ) ↔ ¬ ( ¬ ( 𝑈 ‘ dom 𝑇 ) = ∅ ∧ ¬ ( 𝑈 ‘ dom 𝑇 ) = 1o ∧ ¬ ( 𝑈 ‘ dom 𝑇 ) = 2o ) )
8 6 7 sylib ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ 𝑈 ∈ 𝐵 ) → ¬ ( ¬ ( 𝑈 ‘ dom 𝑇 ) = ∅ ∧ ¬ ( 𝑈 ‘ dom 𝑇 ) = 1o ∧ ¬ ( 𝑈 ‘ dom 𝑇 ) = 2o ) )
9 simpl1 ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ 𝑈 ∈ 𝐵 ) ∧ 𝑇 = ( 𝑈 ↾ dom 𝑇 ) ) → ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 )
10 simpl2 ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ 𝑈 ∈ 𝐵 ) ∧ 𝑇 = ( 𝑈 ↾ dom 𝑇 ) ) → ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) )
11 simpl3 ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ 𝑈 ∈ 𝐵 ) ∧ 𝑇 = ( 𝑈 ↾ dom 𝑇 ) ) → 𝑈 ∈ 𝐵 )
12 simpr ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ 𝑈 ∈ 𝐵 ) ∧ 𝑇 = ( 𝑈 ↾ dom 𝑇 ) ) → 𝑇 = ( 𝑈 ↾ dom 𝑇 ) )
13 12 eqcomd ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ 𝑈 ∈ 𝐵 ) ∧ 𝑇 = ( 𝑈 ↾ dom 𝑇 ) ) → ( 𝑈 ↾ dom 𝑇 ) = 𝑇 )
14 1 noinfbnd1lem4 ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) → ( 𝑈 ‘ dom 𝑇 ) ≠ ∅ )
15 9 10 11 13 14 syl112anc ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ 𝑈 ∈ 𝐵 ) ∧ 𝑇 = ( 𝑈 ↾ dom 𝑇 ) ) → ( 𝑈 ‘ dom 𝑇 ) ≠ ∅ )
16 15 neneqd ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ 𝑈 ∈ 𝐵 ) ∧ 𝑇 = ( 𝑈 ↾ dom 𝑇 ) ) → ¬ ( 𝑈 ‘ dom 𝑇 ) = ∅ )
17 1 noinfbnd1lem3 ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) → ( 𝑈 ‘ dom 𝑇 ) ≠ 1o )
18 9 10 11 13 17 syl112anc ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ 𝑈 ∈ 𝐵 ) ∧ 𝑇 = ( 𝑈 ↾ dom 𝑇 ) ) → ( 𝑈 ‘ dom 𝑇 ) ≠ 1o )
19 18 neneqd ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ 𝑈 ∈ 𝐵 ) ∧ 𝑇 = ( 𝑈 ↾ dom 𝑇 ) ) → ¬ ( 𝑈 ‘ dom 𝑇 ) = 1o )
20 1 noinfbnd1lem5 ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝑈 ∈ 𝐵 ∧ ( 𝑈 ↾ dom 𝑇 ) = 𝑇 ) ) → ( 𝑈 ‘ dom 𝑇 ) ≠ 2o )
21 9 10 11 13 20 syl112anc ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ 𝑈 ∈ 𝐵 ) ∧ 𝑇 = ( 𝑈 ↾ dom 𝑇 ) ) → ( 𝑈 ‘ dom 𝑇 ) ≠ 2o )
22 21 neneqd ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ 𝑈 ∈ 𝐵 ) ∧ 𝑇 = ( 𝑈 ↾ dom 𝑇 ) ) → ¬ ( 𝑈 ‘ dom 𝑇 ) = 2o )
23 16 19 22 3jca ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ 𝑈 ∈ 𝐵 ) ∧ 𝑇 = ( 𝑈 ↾ dom 𝑇 ) ) → ( ¬ ( 𝑈 ‘ dom 𝑇 ) = ∅ ∧ ¬ ( 𝑈 ‘ dom 𝑇 ) = 1o ∧ ¬ ( 𝑈 ‘ dom 𝑇 ) = 2o ) )
24 8 23 mtand ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ 𝑈 ∈ 𝐵 ) → ¬ 𝑇 = ( 𝑈 ↾ dom 𝑇 ) )
25 1 noinfbnd1lem1 ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ 𝑈 ∈ 𝐵 ) → ¬ ( 𝑈 ↾ dom 𝑇 ) <s 𝑇 )
26 1 noinfno ⊢ ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) → 𝑇 ∈ No )
27 26 3ad2ant2 ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ 𝑈 ∈ 𝐵 ) → 𝑇 ∈ No )
28 nodmon ⊢ ( 𝑇 ∈ No → dom 𝑇 ∈ On )
29 27 28 syl ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ 𝑈 ∈ 𝐵 ) → dom 𝑇 ∈ On )
30 noreson ⊢ ( ( 𝑈 ∈ No ∧ dom 𝑇 ∈ On ) → ( 𝑈 ↾ dom 𝑇 ) ∈ No )
31 4 29 30 syl2anc ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ 𝑈 ∈ 𝐵 ) → ( 𝑈 ↾ dom 𝑇 ) ∈ No )
32 sltso ⊢ <s Or No
33 solin ⊢ ( ( <s Or No ∧ ( 𝑇 ∈ No ∧ ( 𝑈 ↾ dom 𝑇 ) ∈ No ) ) → ( 𝑇 <s ( 𝑈 ↾ dom 𝑇 ) ∨ 𝑇 = ( 𝑈 ↾ dom 𝑇 ) ∨ ( 𝑈 ↾ dom 𝑇 ) <s 𝑇 ) )
34 32 33 mpan ⊢ ( ( 𝑇 ∈ No ∧ ( 𝑈 ↾ dom 𝑇 ) ∈ No ) → ( 𝑇 <s ( 𝑈 ↾ dom 𝑇 ) ∨ 𝑇 = ( 𝑈 ↾ dom 𝑇 ) ∨ ( 𝑈 ↾ dom 𝑇 ) <s 𝑇 ) )
35 27 31 34 syl2anc ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ 𝑈 ∈ 𝐵 ) → ( 𝑇 <s ( 𝑈 ↾ dom 𝑇 ) ∨ 𝑇 = ( 𝑈 ↾ dom 𝑇 ) ∨ ( 𝑈 ↾ dom 𝑇 ) <s 𝑇 ) )
36 24 25 35 ecase23d ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ¬ 𝑦 <s 𝑥 ∧ ( 𝐵 ⊆ No ∧ 𝐵 ∈ 𝑉 ) ∧ 𝑈 ∈ 𝐵 ) → 𝑇 <s ( 𝑈 ↾ dom 𝑇 ) )