Metamath Proof Explorer

Theorem nosupbnd1lem6

Description: Lemma for nosupbnd1 . Establish a hard upper bound when there is no maximum. (Contributed by Scott Fenton, 6-Dec-2021)

Ref Expression
Hypothesis nosupbnd1.1 ⊢ 𝑆 = if ( ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 , ( ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) ∪ { ⟨ dom ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) , 2o ⟩ } ) , ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢 ∈ 𝐴 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥 ∃ 𝑢 ∈ 𝐴 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢 ‘ 𝑔 ) = 𝑥 ) ) ) )
Assertion nosupbnd1lem6 ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ 𝑈 ∈ 𝐴 ) → ( 𝑈 ↾ dom 𝑆 ) <s 𝑆 )

Proof

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