Metamath Proof Explorer

Theorem nosupbnd1lem2

Description: Lemma for nosupbnd1 . When there is no maximum, if any member of A is a prolongment of S , then so are all elements of A above it. (Contributed by Scott Fenton, 5-Dec-2021)

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

Proof

Step Hyp Ref Expression
1 nosupbnd1.1 ⊢ 𝑆 = if ( ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 , ( ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) ∪ { ⟨ dom ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) , 2o ⟩ } ) , ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢 ∈ 𝐴 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥 ∃ 𝑢 ∈ 𝐴 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢 ‘ 𝑔 ) = 𝑥 ) ) ) )
2 simp3rr ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ∧ ( 𝑊 ∈ 𝐴 ∧ ¬ 𝑊 <s 𝑈 ) ) ) → ¬ 𝑊 <s 𝑈 )
3 simp2l ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ∧ ( 𝑊 ∈ 𝐴 ∧ ¬ 𝑊 <s 𝑈 ) ) ) → 𝐴 ⊆ No )
4 simp3rl ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ∧ ( 𝑊 ∈ 𝐴 ∧ ¬ 𝑊 <s 𝑈 ) ) ) → 𝑊 ∈ 𝐴 )
5 3 4 sseldd ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ∧ ( 𝑊 ∈ 𝐴 ∧ ¬ 𝑊 <s 𝑈 ) ) ) → 𝑊 ∈ No )
6 simp3ll ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ∧ ( 𝑊 ∈ 𝐴 ∧ ¬ 𝑊 <s 𝑈 ) ) ) → 𝑈 ∈ 𝐴 )
7 3 6 sseldd ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ∧ ( 𝑊 ∈ 𝐴 ∧ ¬ 𝑊 <s 𝑈 ) ) ) → 𝑈 ∈ No )
8 1 nosupno ⊢ ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) → 𝑆 ∈ No )
9 8 3ad2ant2 ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ∧ ( 𝑊 ∈ 𝐴 ∧ ¬ 𝑊 <s 𝑈 ) ) ) → 𝑆 ∈ No )
10 nodmon ⊢ ( 𝑆 ∈ No → dom 𝑆 ∈ On )
11 9 10 syl ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ∧ ( 𝑊 ∈ 𝐴 ∧ ¬ 𝑊 <s 𝑈 ) ) ) → dom 𝑆 ∈ On )
12 ltsres ⊢ ( ( 𝑊 ∈ No ∧ 𝑈 ∈ No ∧ dom 𝑆 ∈ On ) → ( ( 𝑊 ↾ dom 𝑆 ) <s ( 𝑈 ↾ dom 𝑆 ) → 𝑊 <s 𝑈 ) )
13 5 7 11 12 syl3anc ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ∧ ( 𝑊 ∈ 𝐴 ∧ ¬ 𝑊 <s 𝑈 ) ) ) → ( ( 𝑊 ↾ dom 𝑆 ) <s ( 𝑈 ↾ dom 𝑆 ) → 𝑊 <s 𝑈 ) )
14 2 13 mtod ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ∧ ( 𝑊 ∈ 𝐴 ∧ ¬ 𝑊 <s 𝑈 ) ) ) → ¬ ( 𝑊 ↾ dom 𝑆 ) <s ( 𝑈 ↾ dom 𝑆 ) )
15 simp3lr ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ∧ ( 𝑊 ∈ 𝐴 ∧ ¬ 𝑊 <s 𝑈 ) ) ) → ( 𝑈 ↾ dom 𝑆 ) = 𝑆 )
16 15 breq2d ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ∧ ( 𝑊 ∈ 𝐴 ∧ ¬ 𝑊 <s 𝑈 ) ) ) → ( ( 𝑊 ↾ dom 𝑆 ) <s ( 𝑈 ↾ dom 𝑆 ) ↔ ( 𝑊 ↾ dom 𝑆 ) <s 𝑆 ) )
17 14 16 mtbid ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ∧ ( 𝑊 ∈ 𝐴 ∧ ¬ 𝑊 <s 𝑈 ) ) ) → ¬ ( 𝑊 ↾ dom 𝑆 ) <s 𝑆 )
18 1 nosupbnd1lem1 ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ 𝑊 ∈ 𝐴 ) → ¬ 𝑆 <s ( 𝑊 ↾ dom 𝑆 ) )
19 4 18 syld3an3 ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ∧ ( 𝑊 ∈ 𝐴 ∧ ¬ 𝑊 <s 𝑈 ) ) ) → ¬ 𝑆 <s ( 𝑊 ↾ dom 𝑆 ) )
20 noreson ⊢ ( ( 𝑊 ∈ No ∧ dom 𝑆 ∈ On ) → ( 𝑊 ↾ dom 𝑆 ) ∈ No )
21 5 11 20 syl2anc ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ∧ ( 𝑊 ∈ 𝐴 ∧ ¬ 𝑊 <s 𝑈 ) ) ) → ( 𝑊 ↾ dom 𝑆 ) ∈ No )
22 ltsso ⊢ <s Or No
23 sotrieq2 ⊢ ( ( <s Or No ∧ ( ( 𝑊 ↾ dom 𝑆 ) ∈ No ∧ 𝑆 ∈ No ) ) → ( ( 𝑊 ↾ dom 𝑆 ) = 𝑆 ↔ ( ¬ ( 𝑊 ↾ dom 𝑆 ) <s 𝑆 ∧ ¬ 𝑆 <s ( 𝑊 ↾ dom 𝑆 ) ) ) )
24 22 23 mpan ⊢ ( ( ( 𝑊 ↾ dom 𝑆 ) ∈ No ∧ 𝑆 ∈ No ) → ( ( 𝑊 ↾ dom 𝑆 ) = 𝑆 ↔ ( ¬ ( 𝑊 ↾ dom 𝑆 ) <s 𝑆 ∧ ¬ 𝑆 <s ( 𝑊 ↾ dom 𝑆 ) ) ) )
25 21 9 24 syl2anc ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ∧ ( 𝑊 ∈ 𝐴 ∧ ¬ 𝑊 <s 𝑈 ) ) ) → ( ( 𝑊 ↾ dom 𝑆 ) = 𝑆 ↔ ( ¬ ( 𝑊 ↾ dom 𝑆 ) <s 𝑆 ∧ ¬ 𝑆 <s ( 𝑊 ↾ dom 𝑆 ) ) ) )
26 17 19 25 mpbir2and ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ∧ ( 𝑊 ∈ 𝐴 ∧ ¬ 𝑊 <s 𝑈 ) ) ) → ( 𝑊 ↾ dom 𝑆 ) = 𝑆 )