Metamath Proof Explorer

Theorem nosupbnd1lem5

Description: Lemma for nosupbnd1 . If U is a prolongment of S and in A , then ( Udom S ) is not 1o . (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 nosupbnd1lem5 ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) → ( 𝑈 ‘ dom 𝑆 ) ≠ 1o )

Proof

Step Hyp Ref Expression
1 nosupbnd1.1 ⊢ 𝑆 = if ( ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 , ( ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) ∪ { ⟨ dom ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) , 2o ⟩ } ) , ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢 ∈ 𝐴 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥 ∃ 𝑢 ∈ 𝐴 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢 ‘ 𝑔 ) = 𝑥 ) ) ) )
2 1 nosupno ⊢ ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) → 𝑆 ∈ No )
3 2 3ad2ant2 ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) → 𝑆 ∈ No )
4 3 adantl ⊢ ( ( ∀ 𝑧 ∈ 𝐴 ( ¬ 𝑧 <s 𝑈 → ( 𝑧 ‘ dom 𝑆 ) = 1o ) ∧ ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ) → 𝑆 ∈ No )
5 nodmord ⊢ ( 𝑆 ∈ No → Ord dom 𝑆 )
6 ordirr ⊢ ( Ord dom 𝑆 → ¬ dom 𝑆 ∈ dom 𝑆 )
7 4 5 6 3syl ⊢ ( ( ∀ 𝑧 ∈ 𝐴 ( ¬ 𝑧 <s 𝑈 → ( 𝑧 ‘ dom 𝑆 ) = 1o ) ∧ ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ) → ¬ dom 𝑆 ∈ dom 𝑆 )
8 simpr3l ⊢ ( ( ∀ 𝑧 ∈ 𝐴 ( ¬ 𝑧 <s 𝑈 → ( 𝑧 ‘ dom 𝑆 ) = 1o ) ∧ ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ) → 𝑈 ∈ 𝐴 )
9 8 adantr ⊢ ( ( ( ∀ 𝑧 ∈ 𝐴 ( ¬ 𝑧 <s 𝑈 → ( 𝑧 ‘ dom 𝑆 ) = 1o ) ∧ ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = 1o ) → 𝑈 ∈ 𝐴 )
10 ndmfv ⊢ ( ¬ dom 𝑆 ∈ dom 𝑈 → ( 𝑈 ‘ dom 𝑆 ) = ∅ )
11 1oex ⊢ 1o ∈ V
12 11 prid1 ⊢ 1o ∈ { 1o , 2o }
13 12 nosgnn0i ⊢ ∅ ≠ 1o
14 neeq1 ⊢ ( ( 𝑈 ‘ dom 𝑆 ) = ∅ → ( ( 𝑈 ‘ dom 𝑆 ) ≠ 1o ↔ ∅ ≠ 1o ) )
15 13 14 mpbiri ⊢ ( ( 𝑈 ‘ dom 𝑆 ) = ∅ → ( 𝑈 ‘ dom 𝑆 ) ≠ 1o )
16 15 neneqd ⊢ ( ( 𝑈 ‘ dom 𝑆 ) = ∅ → ¬ ( 𝑈 ‘ dom 𝑆 ) = 1o )
17 10 16 syl ⊢ ( ¬ dom 𝑆 ∈ dom 𝑈 → ¬ ( 𝑈 ‘ dom 𝑆 ) = 1o )
18 17 con4i ⊢ ( ( 𝑈 ‘ dom 𝑆 ) = 1o → dom 𝑆 ∈ dom 𝑈 )
19 18 adantl ⊢ ( ( ( ∀ 𝑧 ∈ 𝐴 ( ¬ 𝑧 <s 𝑈 → ( 𝑧 ‘ dom 𝑆 ) = 1o ) ∧ ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = 1o ) → dom 𝑆 ∈ dom 𝑈 )
20 simp2l ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) → 𝐴 ⊆ No )
21 simp3l ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) → 𝑈 ∈ 𝐴 )
22 20 21 sseldd ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) → 𝑈 ∈ No )
23 22 adantr ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = 1o ) → 𝑈 ∈ No )
24 23 adantr ⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = 1o ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 <s 𝑈 ) ∧ ( 𝑧 ‘ dom 𝑆 ) = 1o ) ) → 𝑈 ∈ No )
25 nofun ⊢ ( 𝑈 ∈ No → Fun 𝑈 )
26 24 25 syl ⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = 1o ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 <s 𝑈 ) ∧ ( 𝑧 ‘ dom 𝑆 ) = 1o ) ) → Fun 𝑈 )
27 simpl2l ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = 1o ) → 𝐴 ⊆ No )
28 simpll ⊢ ( ( ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 <s 𝑈 ) ∧ ( 𝑧 ‘ dom 𝑆 ) = 1o ) → 𝑧 ∈ 𝐴 )
29 ssel2 ⊢ ( ( 𝐴 ⊆ No ∧ 𝑧 ∈ 𝐴 ) → 𝑧 ∈ No )
30 27 28 29 syl2an ⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = 1o ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 <s 𝑈 ) ∧ ( 𝑧 ‘ dom 𝑆 ) = 1o ) ) → 𝑧 ∈ No )
31 nofun ⊢ ( 𝑧 ∈ No → Fun 𝑧 )
32 30 31 syl ⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = 1o ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 <s 𝑈 ) ∧ ( 𝑧 ‘ dom 𝑆 ) = 1o ) ) → Fun 𝑧 )
33 simpl3r ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = 1o ) → ( 𝑈 ↾ dom 𝑆 ) = 𝑆 )
34 33 adantr ⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = 1o ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 <s 𝑈 ) ∧ ( 𝑧 ‘ dom 𝑆 ) = 1o ) ) → ( 𝑈 ↾ dom 𝑆 ) = 𝑆 )
35 simpll1 ⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = 1o ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 <s 𝑈 ) ∧ ( 𝑧 ‘ dom 𝑆 ) = 1o ) ) → ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 )
36 simpll2 ⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = 1o ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 <s 𝑈 ) ∧ ( 𝑧 ‘ dom 𝑆 ) = 1o ) ) → ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) )
37 simpll3 ⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = 1o ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 <s 𝑈 ) ∧ ( 𝑧 ‘ dom 𝑆 ) = 1o ) ) → ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) )
38 simprl ⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = 1o ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 <s 𝑈 ) ∧ ( 𝑧 ‘ dom 𝑆 ) = 1o ) ) → ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 <s 𝑈 ) )
39 1 nosupbnd1lem2 ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 <s 𝑈 ) ) ) → ( 𝑧 ↾ dom 𝑆 ) = 𝑆 )
40 35 36 37 38 39 syl112anc ⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = 1o ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 <s 𝑈 ) ∧ ( 𝑧 ‘ dom 𝑆 ) = 1o ) ) → ( 𝑧 ↾ dom 𝑆 ) = 𝑆 )
41 34 40 eqtr4d ⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = 1o ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 <s 𝑈 ) ∧ ( 𝑧 ‘ dom 𝑆 ) = 1o ) ) → ( 𝑈 ↾ dom 𝑆 ) = ( 𝑧 ↾ dom 𝑆 ) )
42 18 adantl ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = 1o ) → dom 𝑆 ∈ dom 𝑈 )
43 42 adantr ⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = 1o ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 <s 𝑈 ) ∧ ( 𝑧 ‘ dom 𝑆 ) = 1o ) ) → dom 𝑆 ∈ dom 𝑈 )
44 ndmfv ⊢ ( ¬ dom 𝑆 ∈ dom 𝑧 → ( 𝑧 ‘ dom 𝑆 ) = ∅ )
45 neeq1 ⊢ ( ( 𝑧 ‘ dom 𝑆 ) = ∅ → ( ( 𝑧 ‘ dom 𝑆 ) ≠ 1o ↔ ∅ ≠ 1o ) )
46 13 45 mpbiri ⊢ ( ( 𝑧 ‘ dom 𝑆 ) = ∅ → ( 𝑧 ‘ dom 𝑆 ) ≠ 1o )
47 46 neneqd ⊢ ( ( 𝑧 ‘ dom 𝑆 ) = ∅ → ¬ ( 𝑧 ‘ dom 𝑆 ) = 1o )
48 44 47 syl ⊢ ( ¬ dom 𝑆 ∈ dom 𝑧 → ¬ ( 𝑧 ‘ dom 𝑆 ) = 1o )
49 48 con4i ⊢ ( ( 𝑧 ‘ dom 𝑆 ) = 1o → dom 𝑆 ∈ dom 𝑧 )
50 49 adantl ⊢ ( ( ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 <s 𝑈 ) ∧ ( 𝑧 ‘ dom 𝑆 ) = 1o ) → dom 𝑆 ∈ dom 𝑧 )
51 50 adantl ⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = 1o ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 <s 𝑈 ) ∧ ( 𝑧 ‘ dom 𝑆 ) = 1o ) ) → dom 𝑆 ∈ dom 𝑧 )
52 simplr ⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = 1o ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 <s 𝑈 ) ∧ ( 𝑧 ‘ dom 𝑆 ) = 1o ) ) → ( 𝑈 ‘ dom 𝑆 ) = 1o )
53 simprr ⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = 1o ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 <s 𝑈 ) ∧ ( 𝑧 ‘ dom 𝑆 ) = 1o ) ) → ( 𝑧 ‘ dom 𝑆 ) = 1o )
54 52 53 eqtr4d ⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = 1o ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 <s 𝑈 ) ∧ ( 𝑧 ‘ dom 𝑆 ) = 1o ) ) → ( 𝑈 ‘ dom 𝑆 ) = ( 𝑧 ‘ dom 𝑆 ) )
55 eqfunressuc ⊢ ( ( ( Fun 𝑈 ∧ Fun 𝑧 ) ∧ ( 𝑈 ↾ dom 𝑆 ) = ( 𝑧 ↾ dom 𝑆 ) ∧ ( dom 𝑆 ∈ dom 𝑈 ∧ dom 𝑆 ∈ dom 𝑧 ∧ ( 𝑈 ‘ dom 𝑆 ) = ( 𝑧 ‘ dom 𝑆 ) ) ) → ( 𝑈 ↾ suc dom 𝑆 ) = ( 𝑧 ↾ suc dom 𝑆 ) )
56 26 32 41 43 51 54 55 syl213anc ⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = 1o ) ∧ ( ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 <s 𝑈 ) ∧ ( 𝑧 ‘ dom 𝑆 ) = 1o ) ) → ( 𝑈 ↾ suc dom 𝑆 ) = ( 𝑧 ↾ suc dom 𝑆 ) )
57 56 expr ⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = 1o ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 <s 𝑈 ) ) → ( ( 𝑧 ‘ dom 𝑆 ) = 1o → ( 𝑈 ↾ suc dom 𝑆 ) = ( 𝑧 ↾ suc dom 𝑆 ) ) )
58 57 expr ⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = 1o ) ∧ 𝑧 ∈ 𝐴 ) → ( ¬ 𝑧 <s 𝑈 → ( ( 𝑧 ‘ dom 𝑆 ) = 1o → ( 𝑈 ↾ suc dom 𝑆 ) = ( 𝑧 ↾ suc dom 𝑆 ) ) ) )
59 58 a2d ⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = 1o ) ∧ 𝑧 ∈ 𝐴 ) → ( ( ¬ 𝑧 <s 𝑈 → ( 𝑧 ‘ dom 𝑆 ) = 1o ) → ( ¬ 𝑧 <s 𝑈 → ( 𝑈 ↾ suc dom 𝑆 ) = ( 𝑧 ↾ suc dom 𝑆 ) ) ) )
60 59 ralimdva ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = 1o ) → ( ∀ 𝑧 ∈ 𝐴 ( ¬ 𝑧 <s 𝑈 → ( 𝑧 ‘ dom 𝑆 ) = 1o ) → ∀ 𝑧 ∈ 𝐴 ( ¬ 𝑧 <s 𝑈 → ( 𝑈 ↾ suc dom 𝑆 ) = ( 𝑧 ↾ suc dom 𝑆 ) ) ) )
61 60 impcom ⊢ ( ( ∀ 𝑧 ∈ 𝐴 ( ¬ 𝑧 <s 𝑈 → ( 𝑧 ‘ dom 𝑆 ) = 1o ) ∧ ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = 1o ) ) → ∀ 𝑧 ∈ 𝐴 ( ¬ 𝑧 <s 𝑈 → ( 𝑈 ↾ suc dom 𝑆 ) = ( 𝑧 ↾ suc dom 𝑆 ) ) )
62 61 anassrs ⊢ ( ( ( ∀ 𝑧 ∈ 𝐴 ( ¬ 𝑧 <s 𝑈 → ( 𝑧 ‘ dom 𝑆 ) = 1o ) ∧ ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = 1o ) → ∀ 𝑧 ∈ 𝐴 ( ¬ 𝑧 <s 𝑈 → ( 𝑈 ↾ suc dom 𝑆 ) = ( 𝑧 ↾ suc dom 𝑆 ) ) )
63 dmeq ⊢ ( 𝑝 = 𝑈 → dom 𝑝 = dom 𝑈 )
64 63 eleq2d ⊢ ( 𝑝 = 𝑈 → ( dom 𝑆 ∈ dom 𝑝 ↔ dom 𝑆 ∈ dom 𝑈 ) )
65 breq2 ⊢ ( 𝑝 = 𝑈 → ( 𝑧 <s 𝑝 ↔ 𝑧 <s 𝑈 ) )
66 65 notbid ⊢ ( 𝑝 = 𝑈 → ( ¬ 𝑧 <s 𝑝 ↔ ¬ 𝑧 <s 𝑈 ) )
67 reseq1 ⊢ ( 𝑝 = 𝑈 → ( 𝑝 ↾ suc dom 𝑆 ) = ( 𝑈 ↾ suc dom 𝑆 ) )
68 67 eqeq1d ⊢ ( 𝑝 = 𝑈 → ( ( 𝑝 ↾ suc dom 𝑆 ) = ( 𝑧 ↾ suc dom 𝑆 ) ↔ ( 𝑈 ↾ suc dom 𝑆 ) = ( 𝑧 ↾ suc dom 𝑆 ) ) )
69 66 68 imbi12d ⊢ ( 𝑝 = 𝑈 → ( ( ¬ 𝑧 <s 𝑝 → ( 𝑝 ↾ suc dom 𝑆 ) = ( 𝑧 ↾ suc dom 𝑆 ) ) ↔ ( ¬ 𝑧 <s 𝑈 → ( 𝑈 ↾ suc dom 𝑆 ) = ( 𝑧 ↾ suc dom 𝑆 ) ) ) )
70 69 ralbidv ⊢ ( 𝑝 = 𝑈 → ( ∀ 𝑧 ∈ 𝐴 ( ¬ 𝑧 <s 𝑝 → ( 𝑝 ↾ suc dom 𝑆 ) = ( 𝑧 ↾ suc dom 𝑆 ) ) ↔ ∀ 𝑧 ∈ 𝐴 ( ¬ 𝑧 <s 𝑈 → ( 𝑈 ↾ suc dom 𝑆 ) = ( 𝑧 ↾ suc dom 𝑆 ) ) ) )
71 64 70 anbi12d ⊢ ( 𝑝 = 𝑈 → ( ( dom 𝑆 ∈ dom 𝑝 ∧ ∀ 𝑧 ∈ 𝐴 ( ¬ 𝑧 <s 𝑝 → ( 𝑝 ↾ suc dom 𝑆 ) = ( 𝑧 ↾ suc dom 𝑆 ) ) ) ↔ ( dom 𝑆 ∈ dom 𝑈 ∧ ∀ 𝑧 ∈ 𝐴 ( ¬ 𝑧 <s 𝑈 → ( 𝑈 ↾ suc dom 𝑆 ) = ( 𝑧 ↾ suc dom 𝑆 ) ) ) ) )
72 71 rspcev ⊢ ( ( 𝑈 ∈ 𝐴 ∧ ( dom 𝑆 ∈ dom 𝑈 ∧ ∀ 𝑧 ∈ 𝐴 ( ¬ 𝑧 <s 𝑈 → ( 𝑈 ↾ suc dom 𝑆 ) = ( 𝑧 ↾ suc dom 𝑆 ) ) ) ) → ∃ 𝑝 ∈ 𝐴 ( dom 𝑆 ∈ dom 𝑝 ∧ ∀ 𝑧 ∈ 𝐴 ( ¬ 𝑧 <s 𝑝 → ( 𝑝 ↾ suc dom 𝑆 ) = ( 𝑧 ↾ suc dom 𝑆 ) ) ) )
73 9 19 62 72 syl12anc ⊢ ( ( ( ∀ 𝑧 ∈ 𝐴 ( ¬ 𝑧 <s 𝑈 → ( 𝑧 ‘ dom 𝑆 ) = 1o ) ∧ ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = 1o ) → ∃ 𝑝 ∈ 𝐴 ( dom 𝑆 ∈ dom 𝑝 ∧ ∀ 𝑧 ∈ 𝐴 ( ¬ 𝑧 <s 𝑝 → ( 𝑝 ↾ suc dom 𝑆 ) = ( 𝑧 ↾ suc dom 𝑆 ) ) ) )
74 simplr1 ⊢ ( ( ( ∀ 𝑧 ∈ 𝐴 ( ¬ 𝑧 <s 𝑈 → ( 𝑧 ‘ dom 𝑆 ) = 1o ) ∧ ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = 1o ) → ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 )
75 1 nosupdm ⊢ ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 → dom 𝑆 = { 𝑎 ∣ ∃ 𝑝 ∈ 𝐴 ( 𝑎 ∈ dom 𝑝 ∧ ∀ 𝑧 ∈ 𝐴 ( ¬ 𝑧 <s 𝑝 → ( 𝑝 ↾ suc 𝑎 ) = ( 𝑧 ↾ suc 𝑎 ) ) ) } )
76 75 eleq2d ⊢ ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 → ( dom 𝑆 ∈ dom 𝑆 ↔ dom 𝑆 ∈ { 𝑎 ∣ ∃ 𝑝 ∈ 𝐴 ( 𝑎 ∈ dom 𝑝 ∧ ∀ 𝑧 ∈ 𝐴 ( ¬ 𝑧 <s 𝑝 → ( 𝑝 ↾ suc 𝑎 ) = ( 𝑧 ↾ suc 𝑎 ) ) ) } ) )
77 74 76 syl ⊢ ( ( ( ∀ 𝑧 ∈ 𝐴 ( ¬ 𝑧 <s 𝑈 → ( 𝑧 ‘ dom 𝑆 ) = 1o ) ∧ ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = 1o ) → ( dom 𝑆 ∈ dom 𝑆 ↔ dom 𝑆 ∈ { 𝑎 ∣ ∃ 𝑝 ∈ 𝐴 ( 𝑎 ∈ dom 𝑝 ∧ ∀ 𝑧 ∈ 𝐴 ( ¬ 𝑧 <s 𝑝 → ( 𝑝 ↾ suc 𝑎 ) = ( 𝑧 ↾ suc 𝑎 ) ) ) } ) )
78 4 adantr ⊢ ( ( ( ∀ 𝑧 ∈ 𝐴 ( ¬ 𝑧 <s 𝑈 → ( 𝑧 ‘ dom 𝑆 ) = 1o ) ∧ ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = 1o ) → 𝑆 ∈ No )
79 nodmon ⊢ ( 𝑆 ∈ No → dom 𝑆 ∈ On )
80 eleq1 ⊢ ( 𝑎 = dom 𝑆 → ( 𝑎 ∈ dom 𝑝 ↔ dom 𝑆 ∈ dom 𝑝 ) )
81 suceq ⊢ ( 𝑎 = dom 𝑆 → suc 𝑎 = suc dom 𝑆 )
82 81 reseq2d ⊢ ( 𝑎 = dom 𝑆 → ( 𝑝 ↾ suc 𝑎 ) = ( 𝑝 ↾ suc dom 𝑆 ) )
83 81 reseq2d ⊢ ( 𝑎 = dom 𝑆 → ( 𝑧 ↾ suc 𝑎 ) = ( 𝑧 ↾ suc dom 𝑆 ) )
84 82 83 eqeq12d ⊢ ( 𝑎 = dom 𝑆 → ( ( 𝑝 ↾ suc 𝑎 ) = ( 𝑧 ↾ suc 𝑎 ) ↔ ( 𝑝 ↾ suc dom 𝑆 ) = ( 𝑧 ↾ suc dom 𝑆 ) ) )
85 84 imbi2d ⊢ ( 𝑎 = dom 𝑆 → ( ( ¬ 𝑧 <s 𝑝 → ( 𝑝 ↾ suc 𝑎 ) = ( 𝑧 ↾ suc 𝑎 ) ) ↔ ( ¬ 𝑧 <s 𝑝 → ( 𝑝 ↾ suc dom 𝑆 ) = ( 𝑧 ↾ suc dom 𝑆 ) ) ) )
86 85 ralbidv ⊢ ( 𝑎 = dom 𝑆 → ( ∀ 𝑧 ∈ 𝐴 ( ¬ 𝑧 <s 𝑝 → ( 𝑝 ↾ suc 𝑎 ) = ( 𝑧 ↾ suc 𝑎 ) ) ↔ ∀ 𝑧 ∈ 𝐴 ( ¬ 𝑧 <s 𝑝 → ( 𝑝 ↾ suc dom 𝑆 ) = ( 𝑧 ↾ suc dom 𝑆 ) ) ) )
87 80 86 anbi12d ⊢ ( 𝑎 = dom 𝑆 → ( ( 𝑎 ∈ dom 𝑝 ∧ ∀ 𝑧 ∈ 𝐴 ( ¬ 𝑧 <s 𝑝 → ( 𝑝 ↾ suc 𝑎 ) = ( 𝑧 ↾ suc 𝑎 ) ) ) ↔ ( dom 𝑆 ∈ dom 𝑝 ∧ ∀ 𝑧 ∈ 𝐴 ( ¬ 𝑧 <s 𝑝 → ( 𝑝 ↾ suc dom 𝑆 ) = ( 𝑧 ↾ suc dom 𝑆 ) ) ) ) )
88 87 rexbidv ⊢ ( 𝑎 = dom 𝑆 → ( ∃ 𝑝 ∈ 𝐴 ( 𝑎 ∈ dom 𝑝 ∧ ∀ 𝑧 ∈ 𝐴 ( ¬ 𝑧 <s 𝑝 → ( 𝑝 ↾ suc 𝑎 ) = ( 𝑧 ↾ suc 𝑎 ) ) ) ↔ ∃ 𝑝 ∈ 𝐴 ( dom 𝑆 ∈ dom 𝑝 ∧ ∀ 𝑧 ∈ 𝐴 ( ¬ 𝑧 <s 𝑝 → ( 𝑝 ↾ suc dom 𝑆 ) = ( 𝑧 ↾ suc dom 𝑆 ) ) ) ) )
89 88 elabg ⊢ ( dom 𝑆 ∈ On → ( dom 𝑆 ∈ { 𝑎 ∣ ∃ 𝑝 ∈ 𝐴 ( 𝑎 ∈ dom 𝑝 ∧ ∀ 𝑧 ∈ 𝐴 ( ¬ 𝑧 <s 𝑝 → ( 𝑝 ↾ suc 𝑎 ) = ( 𝑧 ↾ suc 𝑎 ) ) ) } ↔ ∃ 𝑝 ∈ 𝐴 ( dom 𝑆 ∈ dom 𝑝 ∧ ∀ 𝑧 ∈ 𝐴 ( ¬ 𝑧 <s 𝑝 → ( 𝑝 ↾ suc dom 𝑆 ) = ( 𝑧 ↾ suc dom 𝑆 ) ) ) ) )
90 78 79 89 3syl ⊢ ( ( ( ∀ 𝑧 ∈ 𝐴 ( ¬ 𝑧 <s 𝑈 → ( 𝑧 ‘ dom 𝑆 ) = 1o ) ∧ ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = 1o ) → ( dom 𝑆 ∈ { 𝑎 ∣ ∃ 𝑝 ∈ 𝐴 ( 𝑎 ∈ dom 𝑝 ∧ ∀ 𝑧 ∈ 𝐴 ( ¬ 𝑧 <s 𝑝 → ( 𝑝 ↾ suc 𝑎 ) = ( 𝑧 ↾ suc 𝑎 ) ) ) } ↔ ∃ 𝑝 ∈ 𝐴 ( dom 𝑆 ∈ dom 𝑝 ∧ ∀ 𝑧 ∈ 𝐴 ( ¬ 𝑧 <s 𝑝 → ( 𝑝 ↾ suc dom 𝑆 ) = ( 𝑧 ↾ suc dom 𝑆 ) ) ) ) )
91 77 90 bitrd ⊢ ( ( ( ∀ 𝑧 ∈ 𝐴 ( ¬ 𝑧 <s 𝑈 → ( 𝑧 ‘ dom 𝑆 ) = 1o ) ∧ ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = 1o ) → ( dom 𝑆 ∈ dom 𝑆 ↔ ∃ 𝑝 ∈ 𝐴 ( dom 𝑆 ∈ dom 𝑝 ∧ ∀ 𝑧 ∈ 𝐴 ( ¬ 𝑧 <s 𝑝 → ( 𝑝 ↾ suc dom 𝑆 ) = ( 𝑧 ↾ suc dom 𝑆 ) ) ) ) )
92 73 91 mpbird ⊢ ( ( ( ∀ 𝑧 ∈ 𝐴 ( ¬ 𝑧 <s 𝑈 → ( 𝑧 ‘ dom 𝑆 ) = 1o ) ∧ ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = 1o ) → dom 𝑆 ∈ dom 𝑆 )
93 7 92 mtand ⊢ ( ( ∀ 𝑧 ∈ 𝐴 ( ¬ 𝑧 <s 𝑈 → ( 𝑧 ‘ dom 𝑆 ) = 1o ) ∧ ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ) → ¬ ( 𝑈 ‘ dom 𝑆 ) = 1o )
94 93 neqned ⊢ ( ( ∀ 𝑧 ∈ 𝐴 ( ¬ 𝑧 <s 𝑈 → ( 𝑧 ‘ dom 𝑆 ) = 1o ) ∧ ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ) → ( 𝑈 ‘ dom 𝑆 ) ≠ 1o )
95 rexanali ⊢ ( ∃ 𝑧 ∈ 𝐴 ( ¬ 𝑧 <s 𝑈 ∧ ¬ ( 𝑧 ‘ dom 𝑆 ) = 1o ) ↔ ¬ ∀ 𝑧 ∈ 𝐴 ( ¬ 𝑧 <s 𝑈 → ( 𝑧 ‘ dom 𝑆 ) = 1o ) )
96 simpl ⊢ ( ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 <s 𝑈 ) → 𝑧 ∈ 𝐴 )
97 20 96 29 syl2an ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 <s 𝑈 ) ) → 𝑧 ∈ No )
98 nofv ⊢ ( 𝑧 ∈ No → ( ( 𝑧 ‘ dom 𝑆 ) = ∅ ∨ ( 𝑧 ‘ dom 𝑆 ) = 1o ∨ ( 𝑧 ‘ dom 𝑆 ) = 2o ) )
99 97 98 syl ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 <s 𝑈 ) ) → ( ( 𝑧 ‘ dom 𝑆 ) = ∅ ∨ ( 𝑧 ‘ dom 𝑆 ) = 1o ∨ ( 𝑧 ‘ dom 𝑆 ) = 2o ) )
100 3orel2 ⊢ ( ¬ ( 𝑧 ‘ dom 𝑆 ) = 1o → ( ( ( 𝑧 ‘ dom 𝑆 ) = ∅ ∨ ( 𝑧 ‘ dom 𝑆 ) = 1o ∨ ( 𝑧 ‘ dom 𝑆 ) = 2o ) → ( ( 𝑧 ‘ dom 𝑆 ) = ∅ ∨ ( 𝑧 ‘ dom 𝑆 ) = 2o ) ) )
101 99 100 syl5com ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 <s 𝑈 ) ) → ( ¬ ( 𝑧 ‘ dom 𝑆 ) = 1o → ( ( 𝑧 ‘ dom 𝑆 ) = ∅ ∨ ( 𝑧 ‘ dom 𝑆 ) = 2o ) ) )
102 101 imdistanda ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) → ( ( ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 <s 𝑈 ) ∧ ¬ ( 𝑧 ‘ dom 𝑆 ) = 1o ) → ( ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 <s 𝑈 ) ∧ ( ( 𝑧 ‘ dom 𝑆 ) = ∅ ∨ ( 𝑧 ‘ dom 𝑆 ) = 2o ) ) ) )
103 simpl1 ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 <s 𝑈 ) ) → ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 )
104 simpl2 ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 <s 𝑈 ) ) → ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) )
105 simprl ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 <s 𝑈 ) ) → 𝑧 ∈ 𝐴 )
106 simpl3 ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 <s 𝑈 ) ) → ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) )
107 simpr ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 <s 𝑈 ) ) → ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 <s 𝑈 ) )
108 103 104 106 107 39 syl112anc ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 <s 𝑈 ) ) → ( 𝑧 ↾ dom 𝑆 ) = 𝑆 )
109 1 nosupbnd1lem4 ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑧 ∈ 𝐴 ∧ ( 𝑧 ↾ dom 𝑆 ) = 𝑆 ) ) → ( 𝑧 ‘ dom 𝑆 ) ≠ ∅ )
110 103 104 105 108 109 syl112anc ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 <s 𝑈 ) ) → ( 𝑧 ‘ dom 𝑆 ) ≠ ∅ )
111 110 neneqd ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 <s 𝑈 ) ) → ¬ ( 𝑧 ‘ dom 𝑆 ) = ∅ )
112 111 pm2.21d ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 <s 𝑈 ) ) → ( ( 𝑧 ‘ dom 𝑆 ) = ∅ → ( 𝑈 ‘ dom 𝑆 ) ≠ 1o ) )
113 1 nosupbnd1lem3 ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑧 ∈ 𝐴 ∧ ( 𝑧 ↾ dom 𝑆 ) = 𝑆 ) ) → ( 𝑧 ‘ dom 𝑆 ) ≠ 2o )
114 103 104 105 108 113 syl112anc ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 <s 𝑈 ) ) → ( 𝑧 ‘ dom 𝑆 ) ≠ 2o )
115 114 neneqd ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 <s 𝑈 ) ) → ¬ ( 𝑧 ‘ dom 𝑆 ) = 2o )
116 115 pm2.21d ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 <s 𝑈 ) ) → ( ( 𝑧 ‘ dom 𝑆 ) = 2o → ( 𝑈 ‘ dom 𝑆 ) ≠ 1o ) )
117 112 116 jaod ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 <s 𝑈 ) ) → ( ( ( 𝑧 ‘ dom 𝑆 ) = ∅ ∨ ( 𝑧 ‘ dom 𝑆 ) = 2o ) → ( 𝑈 ‘ dom 𝑆 ) ≠ 1o ) )
118 117 expimpd ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) → ( ( ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 <s 𝑈 ) ∧ ( ( 𝑧 ‘ dom 𝑆 ) = ∅ ∨ ( 𝑧 ‘ dom 𝑆 ) = 2o ) ) → ( 𝑈 ‘ dom 𝑆 ) ≠ 1o ) )
119 102 118 syldc ⊢ ( ( ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 <s 𝑈 ) ∧ ¬ ( 𝑧 ‘ dom 𝑆 ) = 1o ) → ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) → ( 𝑈 ‘ dom 𝑆 ) ≠ 1o ) )
120 119 anasss ⊢ ( ( 𝑧 ∈ 𝐴 ∧ ( ¬ 𝑧 <s 𝑈 ∧ ¬ ( 𝑧 ‘ dom 𝑆 ) = 1o ) ) → ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) → ( 𝑈 ‘ dom 𝑆 ) ≠ 1o ) )
121 120 rexlimiva ⊢ ( ∃ 𝑧 ∈ 𝐴 ( ¬ 𝑧 <s 𝑈 ∧ ¬ ( 𝑧 ‘ dom 𝑆 ) = 1o ) → ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) → ( 𝑈 ‘ dom 𝑆 ) ≠ 1o ) )
122 121 imp ⊢ ( ( ∃ 𝑧 ∈ 𝐴 ( ¬ 𝑧 <s 𝑈 ∧ ¬ ( 𝑧 ‘ dom 𝑆 ) = 1o ) ∧ ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ) → ( 𝑈 ‘ dom 𝑆 ) ≠ 1o )
123 95 122 sylanbr ⊢ ( ( ¬ ∀ 𝑧 ∈ 𝐴 ( ¬ 𝑧 <s 𝑈 → ( 𝑧 ‘ dom 𝑆 ) = 1o ) ∧ ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ) → ( 𝑈 ‘ dom 𝑆 ) ≠ 1o )
124 94 123 pm2.61ian ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) → ( 𝑈 ‘ dom 𝑆 ) ≠ 1o )