Metamath Proof Explorer

Theorem nosupbnd1lem4

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

Proof

Step Hyp Ref Expression
1 nosupbnd1.1 ⊢ 𝑆 = if ( ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 , ( ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) ∪ { ⟨ dom ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) , 2o ⟩ } ) , ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢 ∈ 𝐴 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥 ∃ 𝑢 ∈ 𝐴 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢 ‘ 𝑔 ) = 𝑥 ) ) ) )
2 simpl1 ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑤 ∈ 𝐴 ∧ 𝑈 <s 𝑤 ) ) → ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 )
3 simpl2 ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑤 ∈ 𝐴 ∧ 𝑈 <s 𝑤 ) ) → ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) )
4 simprl ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑤 ∈ 𝐴 ∧ 𝑈 <s 𝑤 ) ) → 𝑤 ∈ 𝐴 )
5 simpl3 ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑤 ∈ 𝐴 ∧ 𝑈 <s 𝑤 ) ) → ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) )
6 simprr ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑤 ∈ 𝐴 ∧ 𝑈 <s 𝑤 ) ) → 𝑈 <s 𝑤 )
7 simp2l ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) → 𝐴 ⊆ No )
8 simp3l ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) → 𝑈 ∈ 𝐴 )
9 7 8 sseldd ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) → 𝑈 ∈ No )
10 simpl2l ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑤 ∈ 𝐴 ∧ 𝑈 <s 𝑤 ) ) → 𝐴 ⊆ No )
11 10 4 sseldd ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑤 ∈ 𝐴 ∧ 𝑈 <s 𝑤 ) ) → 𝑤 ∈ No )
12 sltso ⊢ <s Or No
13 soasym ⊢ ( ( <s Or No ∧ ( 𝑈 ∈ No ∧ 𝑤 ∈ No ) ) → ( 𝑈 <s 𝑤 → ¬ 𝑤 <s 𝑈 ) )
14 12 13 mpan ⊢ ( ( 𝑈 ∈ No ∧ 𝑤 ∈ No ) → ( 𝑈 <s 𝑤 → ¬ 𝑤 <s 𝑈 ) )
15 9 11 14 syl2an2r ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑤 ∈ 𝐴 ∧ 𝑈 <s 𝑤 ) ) → ( 𝑈 <s 𝑤 → ¬ 𝑤 <s 𝑈 ) )
16 6 15 mpd ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑤 ∈ 𝐴 ∧ 𝑈 <s 𝑤 ) ) → ¬ 𝑤 <s 𝑈 )
17 4 16 jca ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑤 ∈ 𝐴 ∧ 𝑈 <s 𝑤 ) ) → ( 𝑤 ∈ 𝐴 ∧ ¬ 𝑤 <s 𝑈 ) )
18 1 nosupbnd1lem2 ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ∧ ( 𝑤 ∈ 𝐴 ∧ ¬ 𝑤 <s 𝑈 ) ) ) → ( 𝑤 ↾ dom 𝑆 ) = 𝑆 )
19 2 3 5 17 18 syl112anc ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑤 ∈ 𝐴 ∧ 𝑈 <s 𝑤 ) ) → ( 𝑤 ↾ dom 𝑆 ) = 𝑆 )
20 1 nosupbnd1lem3 ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑤 ∈ 𝐴 ∧ ( 𝑤 ↾ dom 𝑆 ) = 𝑆 ) ) → ( 𝑤 ‘ dom 𝑆 ) ≠ 2o )
21 2 3 4 19 20 syl112anc ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑤 ∈ 𝐴 ∧ 𝑈 <s 𝑤 ) ) → ( 𝑤 ‘ dom 𝑆 ) ≠ 2o )
22 21 neneqd ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑤 ∈ 𝐴 ∧ 𝑈 <s 𝑤 ) ) → ¬ ( 𝑤 ‘ dom 𝑆 ) = 2o )
23 22 expr ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ 𝑤 ∈ 𝐴 ) → ( 𝑈 <s 𝑤 → ¬ ( 𝑤 ‘ dom 𝑆 ) = 2o ) )
24 imnan ⊢ ( ( 𝑈 <s 𝑤 → ¬ ( 𝑤 ‘ dom 𝑆 ) = 2o ) ↔ ¬ ( 𝑈 <s 𝑤 ∧ ( 𝑤 ‘ dom 𝑆 ) = 2o ) )
25 23 24 sylib ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ 𝑤 ∈ 𝐴 ) → ¬ ( 𝑈 <s 𝑤 ∧ ( 𝑤 ‘ dom 𝑆 ) = 2o ) )
26 25 nrexdv ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) → ¬ ∃ 𝑤 ∈ 𝐴 ( 𝑈 <s 𝑤 ∧ ( 𝑤 ‘ dom 𝑆 ) = 2o ) )
27 simpl3l ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = ∅ ) → 𝑈 ∈ 𝐴 )
28 simpl1 ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = ∅ ) → ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 )
29 breq2 ⊢ ( 𝑤 = 𝑦 → ( 𝑢 <s 𝑤 ↔ 𝑢 <s 𝑦 ) )
30 29 cbvrexvw ⊢ ( ∃ 𝑤 ∈ 𝐴 𝑢 <s 𝑤 ↔ ∃ 𝑦 ∈ 𝐴 𝑢 <s 𝑦 )
31 breq1 ⊢ ( 𝑢 = 𝑥 → ( 𝑢 <s 𝑦 ↔ 𝑥 <s 𝑦 ) )
32 31 rexbidv ⊢ ( 𝑢 = 𝑥 → ( ∃ 𝑦 ∈ 𝐴 𝑢 <s 𝑦 ↔ ∃ 𝑦 ∈ 𝐴 𝑥 <s 𝑦 ) )
33 30 32 syl5bb ⊢ ( 𝑢 = 𝑥 → ( ∃ 𝑤 ∈ 𝐴 𝑢 <s 𝑤 ↔ ∃ 𝑦 ∈ 𝐴 𝑥 <s 𝑦 ) )
34 33 cbvralvw ⊢ ( ∀ 𝑢 ∈ 𝐴 ∃ 𝑤 ∈ 𝐴 𝑢 <s 𝑤 ↔ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 𝑥 <s 𝑦 )
35 dfrex2 ⊢ ( ∃ 𝑦 ∈ 𝐴 𝑥 <s 𝑦 ↔ ¬ ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 )
36 35 ralbii ⊢ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 𝑥 <s 𝑦 ↔ ∀ 𝑥 ∈ 𝐴 ¬ ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 )
37 ralnex ⊢ ( ∀ 𝑥 ∈ 𝐴 ¬ ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ↔ ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 )
38 34 36 37 3bitri ⊢ ( ∀ 𝑢 ∈ 𝐴 ∃ 𝑤 ∈ 𝐴 𝑢 <s 𝑤 ↔ ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 )
39 28 38 sylibr ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = ∅ ) → ∀ 𝑢 ∈ 𝐴 ∃ 𝑤 ∈ 𝐴 𝑢 <s 𝑤 )
40 breq1 ⊢ ( 𝑢 = 𝑈 → ( 𝑢 <s 𝑤 ↔ 𝑈 <s 𝑤 ) )
41 40 rexbidv ⊢ ( 𝑢 = 𝑈 → ( ∃ 𝑤 ∈ 𝐴 𝑢 <s 𝑤 ↔ ∃ 𝑤 ∈ 𝐴 𝑈 <s 𝑤 ) )
42 41 rspcv ⊢ ( 𝑈 ∈ 𝐴 → ( ∀ 𝑢 ∈ 𝐴 ∃ 𝑤 ∈ 𝐴 𝑢 <s 𝑤 → ∃ 𝑤 ∈ 𝐴 𝑈 <s 𝑤 ) )
43 27 39 42 sylc ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = ∅ ) → ∃ 𝑤 ∈ 𝐴 𝑈 <s 𝑤 )
44 simpl2l ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = ∅ ) → 𝐴 ⊆ No )
45 44 27 sseldd ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = ∅ ) → 𝑈 ∈ No )
46 45 adantr ⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = ∅ ) ∧ ( 𝑤 ∈ 𝐴 ∧ 𝑈 <s 𝑤 ) ) → 𝑈 ∈ No )
47 44 adantr ⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = ∅ ) ∧ ( 𝑤 ∈ 𝐴 ∧ 𝑈 <s 𝑤 ) ) → 𝐴 ⊆ No )
48 simprl ⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = ∅ ) ∧ ( 𝑤 ∈ 𝐴 ∧ 𝑈 <s 𝑤 ) ) → 𝑤 ∈ 𝐴 )
49 47 48 sseldd ⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = ∅ ) ∧ ( 𝑤 ∈ 𝐴 ∧ 𝑈 <s 𝑤 ) ) → 𝑤 ∈ No )
50 1 nosupno ⊢ ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) → 𝑆 ∈ No )
51 50 3ad2ant2 ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) → 𝑆 ∈ No )
52 51 adantr ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = ∅ ) → 𝑆 ∈ No )
53 52 adantr ⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = ∅ ) ∧ ( 𝑤 ∈ 𝐴 ∧ 𝑈 <s 𝑤 ) ) → 𝑆 ∈ No )
54 nodmon ⊢ ( 𝑆 ∈ No → dom 𝑆 ∈ On )
55 53 54 syl ⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = ∅ ) ∧ ( 𝑤 ∈ 𝐴 ∧ 𝑈 <s 𝑤 ) ) → dom 𝑆 ∈ On )
56 simpl3r ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = ∅ ) → ( 𝑈 ↾ dom 𝑆 ) = 𝑆 )
57 56 adantr ⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = ∅ ) ∧ ( 𝑤 ∈ 𝐴 ∧ 𝑈 <s 𝑤 ) ) → ( 𝑈 ↾ dom 𝑆 ) = 𝑆 )
58 simpll1 ⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = ∅ ) ∧ ( 𝑤 ∈ 𝐴 ∧ 𝑈 <s 𝑤 ) ) → ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 )
59 simpll2 ⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = ∅ ) ∧ ( 𝑤 ∈ 𝐴 ∧ 𝑈 <s 𝑤 ) ) → ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) )
60 simpll3 ⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = ∅ ) ∧ ( 𝑤 ∈ 𝐴 ∧ 𝑈 <s 𝑤 ) ) → ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) )
61 simprr ⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = ∅ ) ∧ ( 𝑤 ∈ 𝐴 ∧ 𝑈 <s 𝑤 ) ) → 𝑈 <s 𝑤 )
62 45 49 14 syl2an2r ⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = ∅ ) ∧ ( 𝑤 ∈ 𝐴 ∧ 𝑈 <s 𝑤 ) ) → ( 𝑈 <s 𝑤 → ¬ 𝑤 <s 𝑈 ) )
63 61 62 mpd ⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = ∅ ) ∧ ( 𝑤 ∈ 𝐴 ∧ 𝑈 <s 𝑤 ) ) → ¬ 𝑤 <s 𝑈 )
64 48 63 jca ⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = ∅ ) ∧ ( 𝑤 ∈ 𝐴 ∧ 𝑈 <s 𝑤 ) ) → ( 𝑤 ∈ 𝐴 ∧ ¬ 𝑤 <s 𝑈 ) )
65 58 59 60 64 18 syl112anc ⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = ∅ ) ∧ ( 𝑤 ∈ 𝐴 ∧ 𝑈 <s 𝑤 ) ) → ( 𝑤 ↾ dom 𝑆 ) = 𝑆 )
66 57 65 eqtr4d ⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = ∅ ) ∧ ( 𝑤 ∈ 𝐴 ∧ 𝑈 <s 𝑤 ) ) → ( 𝑈 ↾ dom 𝑆 ) = ( 𝑤 ↾ dom 𝑆 ) )
67 simplr ⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = ∅ ) ∧ ( 𝑤 ∈ 𝐴 ∧ 𝑈 <s 𝑤 ) ) → ( 𝑈 ‘ dom 𝑆 ) = ∅ )
68 nolt02o ⊢ ( ( ( 𝑈 ∈ No ∧ 𝑤 ∈ No ∧ dom 𝑆 ∈ On ) ∧ ( ( 𝑈 ↾ dom 𝑆 ) = ( 𝑤 ↾ dom 𝑆 ) ∧ 𝑈 <s 𝑤 ) ∧ ( 𝑈 ‘ dom 𝑆 ) = ∅ ) → ( 𝑤 ‘ dom 𝑆 ) = 2o )
69 46 49 55 66 61 67 68 syl321anc ⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = ∅ ) ∧ ( 𝑤 ∈ 𝐴 ∧ 𝑈 <s 𝑤 ) ) → ( 𝑤 ‘ dom 𝑆 ) = 2o )
70 69 expr ⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = ∅ ) ∧ 𝑤 ∈ 𝐴 ) → ( 𝑈 <s 𝑤 → ( 𝑤 ‘ dom 𝑆 ) = 2o ) )
71 70 ancld ⊢ ( ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = ∅ ) ∧ 𝑤 ∈ 𝐴 ) → ( 𝑈 <s 𝑤 → ( 𝑈 <s 𝑤 ∧ ( 𝑤 ‘ dom 𝑆 ) = 2o ) ) )
72 71 reximdva ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = ∅ ) → ( ∃ 𝑤 ∈ 𝐴 𝑈 <s 𝑤 → ∃ 𝑤 ∈ 𝐴 ( 𝑈 <s 𝑤 ∧ ( 𝑤 ‘ dom 𝑆 ) = 2o ) ) )
73 43 72 mpd ⊢ ( ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) ∧ ( 𝑈 ‘ dom 𝑆 ) = ∅ ) → ∃ 𝑤 ∈ 𝐴 ( 𝑈 <s 𝑤 ∧ ( 𝑤 ‘ dom 𝑆 ) = 2o ) )
74 26 73 mtand ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) → ¬ ( 𝑈 ‘ dom 𝑆 ) = ∅ )
75 74 neqned ⊢ ( ( ¬ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ∧ ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) ∧ ( 𝑈 ∈ 𝐴 ∧ ( 𝑈 ↾ dom 𝑆 ) = 𝑆 ) ) → ( 𝑈 ‘ dom 𝑆 ) ≠ ∅ )