Metamath Proof Explorer

Theorem nosupbnd1lem1

Description: Lemma for nosupbnd1 . Establish a soft upper bound. (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 nosupbnd1lem1 ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ 𝑈 ∈ 𝐴 ) → ¬ 𝑆 <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 simp2l ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ 𝑈 ∈ 𝐴 ) → 𝐴 ⊆ No )
3 simp3 ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ 𝑈 ∈ 𝐴 ) → 𝑈 ∈ 𝐴 )
4 2 3 sseldd ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ 𝑈 ∈ 𝐴 ) → 𝑈 ∈ No )
5 1 nosupno ⊢ ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) → 𝑆 ∈ No )
6 5 3ad2ant2 ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ 𝑈 ∈ 𝐴 ) → 𝑆 ∈ No )
7 nodmon ⊢ ( 𝑆 ∈ No → dom 𝑆 ∈ On )
8 6 7 syl ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ 𝑈 ∈ 𝐴 ) → dom 𝑆 ∈ On )
9 noreson ⊢ ( ( 𝑈 ∈ No ∧ dom 𝑆 ∈ On ) → ( 𝑈 ↾ dom 𝑆 ) ∈ No )
10 4 8 9 syl2anc ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ 𝑈 ∈ 𝐴 ) → ( 𝑈 ↾ dom 𝑆 ) ∈ No )
11 dmres ⊢ dom ( 𝑈 ↾ dom 𝑆 ) = ( dom 𝑆 ∩ dom 𝑈 )
12 inss1 ⊢ ( dom 𝑆 ∩ dom 𝑈 ) ⊆ dom 𝑆
13 11 12 eqsstri ⊢ dom ( 𝑈 ↾ dom 𝑆 ) ⊆ dom 𝑆
14 13 a1i ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ 𝑈 ∈ 𝐴 ) → dom ( 𝑈 ↾ dom 𝑆 ) ⊆ dom 𝑆 )
15 ssidd ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ 𝑈 ∈ 𝐴 ) → dom 𝑆 ⊆ dom 𝑆 )
16 iffalse ⊢ ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 → if ( ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 , ( ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) ∪ { ⟨ dom ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) , 2o ⟩ } ) , ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢 ∈ 𝐴 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥 ∃ 𝑢 ∈ 𝐴 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢 ‘ 𝑔 ) = 𝑥 ) ) ) ) = ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢 ∈ 𝐴 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥 ∃ 𝑢 ∈ 𝐴 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢 ‘ 𝑔 ) = 𝑥 ) ) ) )
17 1 16 syl5eq ⊢ ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 → 𝑆 = ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢 ∈ 𝐴 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥 ∃ 𝑢 ∈ 𝐴 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢 ‘ 𝑔 ) = 𝑥 ) ) ) )
18 17 dmeqd ⊢ ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 → dom 𝑆 = dom ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢 ∈ 𝐴 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥 ∃ 𝑢 ∈ 𝐴 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢 ‘ 𝑔 ) = 𝑥 ) ) ) )
19 iotaex ⊢ ( ℩ 𝑥 ∃ 𝑢 ∈ 𝐴 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢 ‘ 𝑔 ) = 𝑥 ) ) ∈ V
20 eqid ⊢ ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢 ∈ 𝐴 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥 ∃ 𝑢 ∈ 𝐴 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢 ‘ 𝑔 ) = 𝑥 ) ) ) = ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢 ∈ 𝐴 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥 ∃ 𝑢 ∈ 𝐴 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢 ‘ 𝑔 ) = 𝑥 ) ) )
21 19 20 dmmpti ⊢ dom ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢 ∈ 𝐴 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥 ∃ 𝑢 ∈ 𝐴 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢 ‘ 𝑔 ) = 𝑥 ) ) ) = { 𝑦 ∣ ∃ 𝑢 ∈ 𝐴 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) }
22 18 21 eqtrdi ⊢ ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 → dom 𝑆 = { 𝑦 ∣ ∃ 𝑢 ∈ 𝐴 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } )
23 22 eleq2d ⊢ ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 → ( ℎ ∈ dom 𝑆 ↔ ℎ ∈ { 𝑦 ∣ ∃ 𝑢 ∈ 𝐴 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ) )
24 vex ⊢ ℎ ∈ V
25 eleq1w ⊢ ( 𝑦 = ℎ → ( 𝑦 ∈ dom 𝑢 ↔ ℎ ∈ dom 𝑢 ) )
26 suceq ⊢ ( 𝑦 = ℎ → suc 𝑦 = suc ℎ )
27 26 reseq2d ⊢ ( 𝑦 = ℎ → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑢 ↾ suc ℎ ) )
28 26 reseq2d ⊢ ( 𝑦 = ℎ → ( 𝑣 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc ℎ ) )
29 27 28 eqeq12d ⊢ ( 𝑦 = ℎ → ( ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ↔ ( 𝑢 ↾ suc ℎ ) = ( 𝑣 ↾ suc ℎ ) ) )
30 29 imbi2d ⊢ ( 𝑦 = ℎ → ( ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ↔ ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc ℎ ) = ( 𝑣 ↾ suc ℎ ) ) ) )
31 30 ralbidv ⊢ ( 𝑦 = ℎ → ( ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ↔ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc ℎ ) = ( 𝑣 ↾ suc ℎ ) ) ) )
32 25 31 anbi12d ⊢ ( 𝑦 = ℎ → ( ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) ↔ ( ℎ ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc ℎ ) = ( 𝑣 ↾ suc ℎ ) ) ) ) )
33 32 rexbidv ⊢ ( 𝑦 = ℎ → ( ∃ 𝑢 ∈ 𝐴 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) ↔ ∃ 𝑢 ∈ 𝐴 ( ℎ ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc ℎ ) = ( 𝑣 ↾ suc ℎ ) ) ) ) )
34 dmeq ⊢ ( 𝑢 = 𝑝 → dom 𝑢 = dom 𝑝 )
35 34 eleq2d ⊢ ( 𝑢 = 𝑝 → ( ℎ ∈ dom 𝑢 ↔ ℎ ∈ dom 𝑝 ) )
36 breq2 ⊢ ( 𝑢 = 𝑝 → ( 𝑣 <s 𝑢 ↔ 𝑣 <s 𝑝 ) )
37 36 notbid ⊢ ( 𝑢 = 𝑝 → ( ¬ 𝑣 <s 𝑢 ↔ ¬ 𝑣 <s 𝑝 ) )
38 reseq1 ⊢ ( 𝑢 = 𝑝 → ( 𝑢 ↾ suc ℎ ) = ( 𝑝 ↾ suc ℎ ) )
39 38 eqeq1d ⊢ ( 𝑢 = 𝑝 → ( ( 𝑢 ↾ suc ℎ ) = ( 𝑣 ↾ suc ℎ ) ↔ ( 𝑝 ↾ suc ℎ ) = ( 𝑣 ↾ suc ℎ ) ) )
40 37 39 imbi12d ⊢ ( 𝑢 = 𝑝 → ( ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc ℎ ) = ( 𝑣 ↾ suc ℎ ) ) ↔ ( ¬ 𝑣 <s 𝑝 → ( 𝑝 ↾ suc ℎ ) = ( 𝑣 ↾ suc ℎ ) ) ) )
41 40 ralbidv ⊢ ( 𝑢 = 𝑝 → ( ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc ℎ ) = ( 𝑣 ↾ suc ℎ ) ) ↔ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑝 → ( 𝑝 ↾ suc ℎ ) = ( 𝑣 ↾ suc ℎ ) ) ) )
42 35 41 anbi12d ⊢ ( 𝑢 = 𝑝 → ( ( ℎ ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc ℎ ) = ( 𝑣 ↾ suc ℎ ) ) ) ↔ ( ℎ ∈ dom 𝑝 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑝 → ( 𝑝 ↾ suc ℎ ) = ( 𝑣 ↾ suc ℎ ) ) ) ) )
43 42 cbvrexvw ⊢ ( ∃ 𝑢 ∈ 𝐴 ( ℎ ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc ℎ ) = ( 𝑣 ↾ suc ℎ ) ) ) ↔ ∃ 𝑝 ∈ 𝐴 ( ℎ ∈ dom 𝑝 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑝 → ( 𝑝 ↾ suc ℎ ) = ( 𝑣 ↾ suc ℎ ) ) ) )
44 33 43 bitrdi ⊢ ( 𝑦 = ℎ → ( ∃ 𝑢 ∈ 𝐴 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) ↔ ∃ 𝑝 ∈ 𝐴 ( ℎ ∈ dom 𝑝 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑝 → ( 𝑝 ↾ suc ℎ ) = ( 𝑣 ↾ suc ℎ ) ) ) ) )
45 24 44 elab ⊢ ( ℎ ∈ { 𝑦 ∣ ∃ 𝑢 ∈ 𝐴 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↔ ∃ 𝑝 ∈ 𝐴 ( ℎ ∈ dom 𝑝 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑝 → ( 𝑝 ↾ suc ℎ ) = ( 𝑣 ↾ suc ℎ ) ) ) )
46 23 45 bitrdi ⊢ ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 → ( ℎ ∈ dom 𝑆 ↔ ∃ 𝑝 ∈ 𝐴 ( ℎ ∈ dom 𝑝 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑝 → ( 𝑝 ↾ suc ℎ ) = ( 𝑣 ↾ suc ℎ ) ) ) ) )
47 46 3ad2ant1 ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ 𝑈 ∈ 𝐴 ) → ( ℎ ∈ dom 𝑆 ↔ ∃ 𝑝 ∈ 𝐴 ( ℎ ∈ dom 𝑝 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑝 → ( 𝑝 ↾ suc ℎ ) = ( 𝑣 ↾ suc ℎ ) ) ) ) )
48 simpl1 ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( ℎ ∈ dom 𝑝 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑝 → ( 𝑝 ↾ suc ℎ ) = ( 𝑣 ↾ suc ℎ ) ) ) ) ) → ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 )
49 simpl2 ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( ℎ ∈ dom 𝑝 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑝 → ( 𝑝 ↾ suc ℎ ) = ( 𝑣 ↾ suc ℎ ) ) ) ) ) → ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) )
50 simprl ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( ℎ ∈ dom 𝑝 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑝 → ( 𝑝 ↾ suc ℎ ) = ( 𝑣 ↾ suc ℎ ) ) ) ) ) → 𝑝 ∈ 𝐴 )
51 simprrl ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( ℎ ∈ dom 𝑝 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑝 → ( 𝑝 ↾ suc ℎ ) = ( 𝑣 ↾ suc ℎ ) ) ) ) ) → ℎ ∈ dom 𝑝 )
52 simprrr ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( ℎ ∈ dom 𝑝 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑝 → ( 𝑝 ↾ suc ℎ ) = ( 𝑣 ↾ suc ℎ ) ) ) ) ) → ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑝 → ( 𝑝 ↾ suc ℎ ) = ( 𝑣 ↾ suc ℎ ) ) )
53 1 nosupres ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑝 ∈ 𝐴 ∧ ℎ ∈ dom 𝑝 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑝 → ( 𝑝 ↾ suc ℎ ) = ( 𝑣 ↾ suc ℎ ) ) ) ) → ( 𝑆 ↾ suc ℎ ) = ( 𝑝 ↾ suc ℎ ) )
54 48 49 50 51 52 53 syl113anc ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( ℎ ∈ dom 𝑝 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑝 → ( 𝑝 ↾ suc ℎ ) = ( 𝑣 ↾ suc ℎ ) ) ) ) ) → ( 𝑆 ↾ suc ℎ ) = ( 𝑝 ↾ suc ℎ ) )
55 simpl2l ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( ℎ ∈ dom 𝑝 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑝 → ( 𝑝 ↾ suc ℎ ) = ( 𝑣 ↾ suc ℎ ) ) ) ) ) → 𝐴 ⊆ No )
56 55 50 sseldd ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( ℎ ∈ dom 𝑝 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑝 → ( 𝑝 ↾ suc ℎ ) = ( 𝑣 ↾ suc ℎ ) ) ) ) ) → 𝑝 ∈ No )
57 4 adantr ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( ℎ ∈ dom 𝑝 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑝 → ( 𝑝 ↾ suc ℎ ) = ( 𝑣 ↾ suc ℎ ) ) ) ) ) → 𝑈 ∈ No )
58 sltso ⊢ <s Or No
59 soasym ⊢ ( ( <s Or No ∧ ( 𝑝 ∈ No ∧ 𝑈 ∈ No ) ) → ( 𝑝 <s 𝑈 → ¬ 𝑈 <s 𝑝 ) )
60 58 59 mpan ⊢ ( ( 𝑝 ∈ No ∧ 𝑈 ∈ No ) → ( 𝑝 <s 𝑈 → ¬ 𝑈 <s 𝑝 ) )
61 56 57 60 syl2anc ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( ℎ ∈ dom 𝑝 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑝 → ( 𝑝 ↾ suc ℎ ) = ( 𝑣 ↾ suc ℎ ) ) ) ) ) → ( 𝑝 <s 𝑈 → ¬ 𝑈 <s 𝑝 ) )
62 simpl3 ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( ℎ ∈ dom 𝑝 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑝 → ( 𝑝 ↾ suc ℎ ) = ( 𝑣 ↾ suc ℎ ) ) ) ) ) → 𝑈 ∈ 𝐴 )
63 breq1 ⊢ ( 𝑣 = 𝑈 → ( 𝑣 <s 𝑝 ↔ 𝑈 <s 𝑝 ) )
64 63 notbid ⊢ ( 𝑣 = 𝑈 → ( ¬ 𝑣 <s 𝑝 ↔ ¬ 𝑈 <s 𝑝 ) )
65 reseq1 ⊢ ( 𝑣 = 𝑈 → ( 𝑣 ↾ suc ℎ ) = ( 𝑈 ↾ suc ℎ ) )
66 65 eqeq2d ⊢ ( 𝑣 = 𝑈 → ( ( 𝑝 ↾ suc ℎ ) = ( 𝑣 ↾ suc ℎ ) ↔ ( 𝑝 ↾ suc ℎ ) = ( 𝑈 ↾ suc ℎ ) ) )
67 64 66 imbi12d ⊢ ( 𝑣 = 𝑈 → ( ( ¬ 𝑣 <s 𝑝 → ( 𝑝 ↾ suc ℎ ) = ( 𝑣 ↾ suc ℎ ) ) ↔ ( ¬ 𝑈 <s 𝑝 → ( 𝑝 ↾ suc ℎ ) = ( 𝑈 ↾ suc ℎ ) ) ) )
68 67 rspcv ⊢ ( 𝑈 ∈ 𝐴 → ( ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑝 → ( 𝑝 ↾ suc ℎ ) = ( 𝑣 ↾ suc ℎ ) ) → ( ¬ 𝑈 <s 𝑝 → ( 𝑝 ↾ suc ℎ ) = ( 𝑈 ↾ suc ℎ ) ) ) )
69 62 52 68 sylc ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( ℎ ∈ dom 𝑝 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑝 → ( 𝑝 ↾ suc ℎ ) = ( 𝑣 ↾ suc ℎ ) ) ) ) ) → ( ¬ 𝑈 <s 𝑝 → ( 𝑝 ↾ suc ℎ ) = ( 𝑈 ↾ suc ℎ ) ) )
70 61 69 syld ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( ℎ ∈ dom 𝑝 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑝 → ( 𝑝 ↾ suc ℎ ) = ( 𝑣 ↾ suc ℎ ) ) ) ) ) → ( 𝑝 <s 𝑈 → ( 𝑝 ↾ suc ℎ ) = ( 𝑈 ↾ suc ℎ ) ) )
71 70 imp ⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( ℎ ∈ dom 𝑝 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑝 → ( 𝑝 ↾ suc ℎ ) = ( 𝑣 ↾ suc ℎ ) ) ) ) ) ∧ 𝑝 <s 𝑈 ) → ( 𝑝 ↾ suc ℎ ) = ( 𝑈 ↾ suc ℎ ) )
72 nodmon ⊢ ( 𝑝 ∈ No → dom 𝑝 ∈ On )
73 56 72 syl ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( ℎ ∈ dom 𝑝 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑝 → ( 𝑝 ↾ suc ℎ ) = ( 𝑣 ↾ suc ℎ ) ) ) ) ) → dom 𝑝 ∈ On )
74 onelon ⊢ ( ( dom 𝑝 ∈ On ∧ ℎ ∈ dom 𝑝 ) → ℎ ∈ On )
75 73 51 74 syl2anc ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( ℎ ∈ dom 𝑝 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑝 → ( 𝑝 ↾ suc ℎ ) = ( 𝑣 ↾ suc ℎ ) ) ) ) ) → ℎ ∈ On )
76 sucelon ⊢ ( ℎ ∈ On ↔ suc ℎ ∈ On )
77 75 76 sylib ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( ℎ ∈ dom 𝑝 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑝 → ( 𝑝 ↾ suc ℎ ) = ( 𝑣 ↾ suc ℎ ) ) ) ) ) → suc ℎ ∈ On )
78 noreson ⊢ ( ( 𝑈 ∈ No ∧ suc ℎ ∈ On ) → ( 𝑈 ↾ suc ℎ ) ∈ No )
79 57 77 78 syl2anc ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( ℎ ∈ dom 𝑝 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑝 → ( 𝑝 ↾ suc ℎ ) = ( 𝑣 ↾ suc ℎ ) ) ) ) ) → ( 𝑈 ↾ suc ℎ ) ∈ No )
80 sonr ⊢ ( ( <s Or No ∧ ( 𝑈 ↾ suc ℎ ) ∈ No ) → ¬ ( 𝑈 ↾ suc ℎ ) <s ( 𝑈 ↾ suc ℎ ) )
81 58 80 mpan ⊢ ( ( 𝑈 ↾ suc ℎ ) ∈ No → ¬ ( 𝑈 ↾ suc ℎ ) <s ( 𝑈 ↾ suc ℎ ) )
82 79 81 syl ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( ℎ ∈ dom 𝑝 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑝 → ( 𝑝 ↾ suc ℎ ) = ( 𝑣 ↾ suc ℎ ) ) ) ) ) → ¬ ( 𝑈 ↾ suc ℎ ) <s ( 𝑈 ↾ suc ℎ ) )
83 82 adantr ⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( ℎ ∈ dom 𝑝 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑝 → ( 𝑝 ↾ suc ℎ ) = ( 𝑣 ↾ suc ℎ ) ) ) ) ) ∧ 𝑝 <s 𝑈 ) → ¬ ( 𝑈 ↾ suc ℎ ) <s ( 𝑈 ↾ suc ℎ ) )
84 71 83 eqnbrtrd ⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( ℎ ∈ dom 𝑝 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑝 → ( 𝑝 ↾ suc ℎ ) = ( 𝑣 ↾ suc ℎ ) ) ) ) ) ∧ 𝑝 <s 𝑈 ) → ¬ ( 𝑝 ↾ suc ℎ ) <s ( 𝑈 ↾ suc ℎ ) )
85 84 ex ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( ℎ ∈ dom 𝑝 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑝 → ( 𝑝 ↾ suc ℎ ) = ( 𝑣 ↾ suc ℎ ) ) ) ) ) → ( 𝑝 <s 𝑈 → ¬ ( 𝑝 ↾ suc ℎ ) <s ( 𝑈 ↾ suc ℎ ) ) )
86 sltres ⊢ ( ( 𝑝 ∈ No ∧ 𝑈 ∈ No ∧ suc ℎ ∈ On ) → ( ( 𝑝 ↾ suc ℎ ) <s ( 𝑈 ↾ suc ℎ ) → 𝑝 <s 𝑈 ) )
87 56 57 77 86 syl3anc ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( ℎ ∈ dom 𝑝 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑝 → ( 𝑝 ↾ suc ℎ ) = ( 𝑣 ↾ suc ℎ ) ) ) ) ) → ( ( 𝑝 ↾ suc ℎ ) <s ( 𝑈 ↾ suc ℎ ) → 𝑝 <s 𝑈 ) )
88 87 con3d ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( ℎ ∈ dom 𝑝 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑝 → ( 𝑝 ↾ suc ℎ ) = ( 𝑣 ↾ suc ℎ ) ) ) ) ) → ( ¬ 𝑝 <s 𝑈 → ¬ ( 𝑝 ↾ suc ℎ ) <s ( 𝑈 ↾ suc ℎ ) ) )
89 85 88 pm2.61d ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( ℎ ∈ dom 𝑝 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑝 → ( 𝑝 ↾ suc ℎ ) = ( 𝑣 ↾ suc ℎ ) ) ) ) ) → ¬ ( 𝑝 ↾ suc ℎ ) <s ( 𝑈 ↾ suc ℎ ) )
90 54 89 eqnbrtrd ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ 𝑈 ∈ 𝐴 ) ∧ ( 𝑝 ∈ 𝐴 ∧ ( ℎ ∈ dom 𝑝 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑝 → ( 𝑝 ↾ suc ℎ ) = ( 𝑣 ↾ suc ℎ ) ) ) ) ) → ¬ ( 𝑆 ↾ suc ℎ ) <s ( 𝑈 ↾ suc ℎ ) )
91 90 rexlimdvaa ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ 𝑈 ∈ 𝐴 ) → ( ∃ 𝑝 ∈ 𝐴 ( ℎ ∈ dom 𝑝 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑝 → ( 𝑝 ↾ suc ℎ ) = ( 𝑣 ↾ suc ℎ ) ) ) → ¬ ( 𝑆 ↾ suc ℎ ) <s ( 𝑈 ↾ suc ℎ ) ) )
92 47 91 sylbid ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ 𝑈 ∈ 𝐴 ) → ( ℎ ∈ dom 𝑆 → ¬ ( 𝑆 ↾ suc ℎ ) <s ( 𝑈 ↾ suc ℎ ) ) )
93 92 imp ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ 𝑈 ∈ 𝐴 ) ∧ ℎ ∈ dom 𝑆 ) → ¬ ( 𝑆 ↾ suc ℎ ) <s ( 𝑈 ↾ suc ℎ ) )
94 nodmord ⊢ ( 𝑆 ∈ No → Ord dom 𝑆 )
95 ordsucss ⊢ ( Ord dom 𝑆 → ( ℎ ∈ dom 𝑆 → suc ℎ ⊆ dom 𝑆 ) )
96 6 94 95 3syl ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ 𝑈 ∈ 𝐴 ) → ( ℎ ∈ dom 𝑆 → suc ℎ ⊆ dom 𝑆 ) )
97 96 imp ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ 𝑈 ∈ 𝐴 ) ∧ ℎ ∈ dom 𝑆 ) → suc ℎ ⊆ dom 𝑆 )
98 97 resabs1d ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ 𝑈 ∈ 𝐴 ) ∧ ℎ ∈ dom 𝑆 ) → ( ( 𝑈 ↾ dom 𝑆 ) ↾ suc ℎ ) = ( 𝑈 ↾ suc ℎ ) )
99 98 breq2d ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ 𝑈 ∈ 𝐴 ) ∧ ℎ ∈ dom 𝑆 ) → ( ( 𝑆 ↾ suc ℎ ) <s ( ( 𝑈 ↾ dom 𝑆 ) ↾ suc ℎ ) ↔ ( 𝑆 ↾ suc ℎ ) <s ( 𝑈 ↾ suc ℎ ) ) )
100 93 99 mtbird ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ 𝑈 ∈ 𝐴 ) ∧ ℎ ∈ dom 𝑆 ) → ¬ ( 𝑆 ↾ suc ℎ ) <s ( ( 𝑈 ↾ dom 𝑆 ) ↾ suc ℎ ) )
101 100 ralrimiva ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ 𝑈 ∈ 𝐴 ) → ∀ ℎ ∈ dom 𝑆 ¬ ( 𝑆 ↾ suc ℎ ) <s ( ( 𝑈 ↾ dom 𝑆 ) ↾ suc ℎ ) )
102 noresle ⊢ ( ( ( ( 𝑈 ↾ dom 𝑆 ) ∈ No ∧ 𝑆 ∈ No ) ∧ ( dom ( 𝑈 ↾ dom 𝑆 ) ⊆ dom 𝑆 ∧ dom 𝑆 ⊆ dom 𝑆 ∧ ∀ ℎ ∈ dom 𝑆 ¬ ( 𝑆 ↾ suc ℎ ) <s ( ( 𝑈 ↾ dom 𝑆 ) ↾ suc ℎ ) ) ) → ¬ 𝑆 <s ( 𝑈 ↾ dom 𝑆 ) )
103 10 6 14 15 101 102 syl23anc ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ 𝑈 ∈ 𝐴 ) → ¬ 𝑆 <s ( 𝑈 ↾ dom 𝑆 ) )