Metamath Proof Explorer

Theorem n0sfincut

Description: The simplest number greater than a finite set of non-negative surreal integers is a non-negative surreal integer. (Contributed by Scott Fenton, 5-Nov-2025)

Ref Expression
Assertion n0sfincut ( ( 𝐴 ⊆ ℕ0s ∧ 𝐴 ∈ Fin ) → ( 𝐴 |s ∅ ) ∈ ℕ0s )

Proof

Step Hyp Ref Expression
1 oveq1 ⊢ ( 𝐴 = ∅ → ( 𝐴 |s ∅ ) = ( ∅ |s ∅ ) )
2 df-0s ⊢ 0s = ( ∅ |s ∅ )
3 0n0s ⊢ 0s ∈ ℕ0s
4 2 3 eqeltrri ⊢ ( ∅ |s ∅ ) ∈ ℕ0s
5 1 4 eqeltrdi ⊢ ( 𝐴 = ∅ → ( 𝐴 |s ∅ ) ∈ ℕ0s )
6 5 a1d ⊢ ( 𝐴 = ∅ → ( ( 𝐴 ⊆ ℕ0s ∧ 𝐴 ∈ Fin ) → ( 𝐴 |s ∅ ) ∈ ℕ0s ) )
7 n0ssno ⊢ ℕ0s ⊆ No
8 sstr ⊢ ( ( 𝐴 ⊆ ℕ0s ∧ ℕ0s ⊆ No ) → 𝐴 ⊆ No )
9 7 8 mpan2 ⊢ ( 𝐴 ⊆ ℕ0s → 𝐴 ⊆ No )
10 sltso ⊢ <s Or No
11 soss ⊢ ( 𝐴 ⊆ No → ( <s Or No → <s Or 𝐴 ) )
12 9 10 11 mpisyl ⊢ ( 𝐴 ⊆ ℕ0s → <s Or 𝐴 )
13 12 ad2antrl ⊢ ( ( 𝐴 ≠ ∅ ∧ ( 𝐴 ⊆ ℕ0s ∧ 𝐴 ∈ Fin ) ) → <s Or 𝐴 )
14 simprr ⊢ ( ( 𝐴 ≠ ∅ ∧ ( 𝐴 ⊆ ℕ0s ∧ 𝐴 ∈ Fin ) ) → 𝐴 ∈ Fin )
15 simpl ⊢ ( ( 𝐴 ≠ ∅ ∧ ( 𝐴 ⊆ ℕ0s ∧ 𝐴 ∈ Fin ) ) → 𝐴 ≠ ∅ )
16 fimax2g ⊢ ( ( <s Or 𝐴 ∧ 𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ) → ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 )
17 13 14 15 16 syl3anc ⊢ ( ( 𝐴 ≠ ∅ ∧ ( 𝐴 ⊆ ℕ0s ∧ 𝐴 ∈ Fin ) ) → ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 )
18 9 ad2antrl ⊢ ( ( 𝐴 ≠ ∅ ∧ ( 𝐴 ⊆ ℕ0s ∧ 𝐴 ∈ Fin ) ) → 𝐴 ⊆ No )
19 18 adantr ⊢ ( ( ( 𝐴 ≠ ∅ ∧ ( 𝐴 ⊆ ℕ0s ∧ 𝐴 ∈ Fin ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝐴 ⊆ No )
20 19 sselda ⊢ ( ( ( ( 𝐴 ≠ ∅ ∧ ( 𝐴 ⊆ ℕ0s ∧ 𝐴 ∈ Fin ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ No )
21 18 sselda ⊢ ( ( ( 𝐴 ≠ ∅ ∧ ( 𝐴 ⊆ ℕ0s ∧ 𝐴 ∈ Fin ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ No )
22 21 adantr ⊢ ( ( ( ( 𝐴 ≠ ∅ ∧ ( 𝐴 ⊆ ℕ0s ∧ 𝐴 ∈ Fin ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → 𝑥 ∈ No )
23 slenlt ⊢ ( ( 𝑦 ∈ No ∧ 𝑥 ∈ No ) → ( 𝑦 ≤s 𝑥 ↔ ¬ 𝑥 <s 𝑦 ) )
24 20 22 23 syl2anc ⊢ ( ( ( ( 𝐴 ≠ ∅ ∧ ( 𝐴 ⊆ ℕ0s ∧ 𝐴 ∈ Fin ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → ( 𝑦 ≤s 𝑥 ↔ ¬ 𝑥 <s 𝑦 ) )
25 24 ralbidva ⊢ ( ( ( 𝐴 ≠ ∅ ∧ ( 𝐴 ⊆ ℕ0s ∧ 𝐴 ∈ Fin ) ) ∧ 𝑥 ∈ 𝐴 ) → ( ∀ 𝑦 ∈ 𝐴 𝑦 ≤s 𝑥 ↔ ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) )
26 simpl ⊢ ( ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 𝑦 ≤s 𝑥 ) → 𝑥 ∈ 𝐴 )
27 ssel2 ⊢ ( ( 𝐴 ⊆ No ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ No )
28 18 26 27 syl2an ⊢ ( ( ( 𝐴 ≠ ∅ ∧ ( 𝐴 ⊆ ℕ0s ∧ 𝐴 ∈ Fin ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 𝑦 ≤s 𝑥 ) ) → 𝑥 ∈ No )
29 snelpwi ⊢ ( 𝑥 ∈ No → { 𝑥 } ∈ 𝒫 No )
30 nulssgt ⊢ ( { 𝑥 } ∈ 𝒫 No → { 𝑥 } <<s ∅ )
31 28 29 30 3syl ⊢ ( ( ( 𝐴 ≠ ∅ ∧ ( 𝐴 ⊆ ℕ0s ∧ 𝐴 ∈ Fin ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 𝑦 ≤s 𝑥 ) ) → { 𝑥 } <<s ∅ )
32 breq2 ⊢ ( 𝑤 = 𝑥 → ( 𝑥 ≤s 𝑤 ↔ 𝑥 ≤s 𝑥 ) )
33 simprl ⊢ ( ( ( 𝐴 ≠ ∅ ∧ ( 𝐴 ⊆ ℕ0s ∧ 𝐴 ∈ Fin ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 𝑦 ≤s 𝑥 ) ) → 𝑥 ∈ 𝐴 )
34 slerflex ⊢ ( 𝑥 ∈ No → 𝑥 ≤s 𝑥 )
35 28 34 syl ⊢ ( ( ( 𝐴 ≠ ∅ ∧ ( 𝐴 ⊆ ℕ0s ∧ 𝐴 ∈ Fin ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 𝑦 ≤s 𝑥 ) ) → 𝑥 ≤s 𝑥 )
36 32 33 35 rspcedvdw ⊢ ( ( ( 𝐴 ≠ ∅ ∧ ( 𝐴 ⊆ ℕ0s ∧ 𝐴 ∈ Fin ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 𝑦 ≤s 𝑥 ) ) → ∃ 𝑤 ∈ 𝐴 𝑥 ≤s 𝑤 )
37 vex ⊢ 𝑥 ∈ V
38 breq1 ⊢ ( 𝑧 = 𝑥 → ( 𝑧 ≤s 𝑤 ↔ 𝑥 ≤s 𝑤 ) )
39 38 rexbidv ⊢ ( 𝑧 = 𝑥 → ( ∃ 𝑤 ∈ 𝐴 𝑧 ≤s 𝑤 ↔ ∃ 𝑤 ∈ 𝐴 𝑥 ≤s 𝑤 ) )
40 37 39 ralsn ⊢ ( ∀ 𝑧 ∈ { 𝑥 } ∃ 𝑤 ∈ 𝐴 𝑧 ≤s 𝑤 ↔ ∃ 𝑤 ∈ 𝐴 𝑥 ≤s 𝑤 )
41 36 40 sylibr ⊢ ( ( ( 𝐴 ≠ ∅ ∧ ( 𝐴 ⊆ ℕ0s ∧ 𝐴 ∈ Fin ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 𝑦 ≤s 𝑥 ) ) → ∀ 𝑧 ∈ { 𝑥 } ∃ 𝑤 ∈ 𝐴 𝑧 ≤s 𝑤 )
42 ral0 ⊢ ∀ 𝑧 ∈ ∅ ∃ 𝑤 ∈ ∅ 𝑤 ≤s 𝑧
43 42 a1i ⊢ ( ( ( 𝐴 ≠ ∅ ∧ ( 𝐴 ⊆ ℕ0s ∧ 𝐴 ∈ Fin ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 𝑦 ≤s 𝑥 ) ) → ∀ 𝑧 ∈ ∅ ∃ 𝑤 ∈ ∅ 𝑤 ≤s 𝑧 )
44 simplrr ⊢ ( ( ( 𝐴 ≠ ∅ ∧ ( 𝐴 ⊆ ℕ0s ∧ 𝐴 ∈ Fin ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 𝑦 ≤s 𝑥 ) ) → 𝐴 ∈ Fin )
45 snex ⊢ { ( { 𝑥 } |s ∅ ) } ∈ V
46 45 a1i ⊢ ( ( ( 𝐴 ≠ ∅ ∧ ( 𝐴 ⊆ ℕ0s ∧ 𝐴 ∈ Fin ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 𝑦 ≤s 𝑥 ) ) → { ( { 𝑥 } |s ∅ ) } ∈ V )
47 18 adantr ⊢ ( ( ( 𝐴 ≠ ∅ ∧ ( 𝐴 ⊆ ℕ0s ∧ 𝐴 ∈ Fin ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 𝑦 ≤s 𝑥 ) ) → 𝐴 ⊆ No )
48 31 scutcld ⊢ ( ( ( 𝐴 ≠ ∅ ∧ ( 𝐴 ⊆ ℕ0s ∧ 𝐴 ∈ Fin ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 𝑦 ≤s 𝑥 ) ) → ( { 𝑥 } |s ∅ ) ∈ No )
49 48 snssd ⊢ ( ( ( 𝐴 ≠ ∅ ∧ ( 𝐴 ⊆ ℕ0s ∧ 𝐴 ∈ Fin ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 𝑦 ≤s 𝑥 ) ) → { ( { 𝑥 } |s ∅ ) } ⊆ No )
50 47 sselda ⊢ ( ( ( ( 𝐴 ≠ ∅ ∧ ( 𝐴 ⊆ ℕ0s ∧ 𝐴 ∈ Fin ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 𝑦 ≤s 𝑥 ) ) ∧ 𝑧 ∈ 𝐴 ) → 𝑧 ∈ No )
51 28 adantr ⊢ ( ( ( ( 𝐴 ≠ ∅ ∧ ( 𝐴 ⊆ ℕ0s ∧ 𝐴 ∈ Fin ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 𝑦 ≤s 𝑥 ) ) ∧ 𝑧 ∈ 𝐴 ) → 𝑥 ∈ No )
52 48 adantr ⊢ ( ( ( ( 𝐴 ≠ ∅ ∧ ( 𝐴 ⊆ ℕ0s ∧ 𝐴 ∈ Fin ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 𝑦 ≤s 𝑥 ) ) ∧ 𝑧 ∈ 𝐴 ) → ( { 𝑥 } |s ∅ ) ∈ No )
53 breq1 ⊢ ( 𝑦 = 𝑧 → ( 𝑦 ≤s 𝑥 ↔ 𝑧 ≤s 𝑥 ) )
54 simplrr ⊢ ( ( ( ( 𝐴 ≠ ∅ ∧ ( 𝐴 ⊆ ℕ0s ∧ 𝐴 ∈ Fin ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 𝑦 ≤s 𝑥 ) ) ∧ 𝑧 ∈ 𝐴 ) → ∀ 𝑦 ∈ 𝐴 𝑦 ≤s 𝑥 )
55 simpr ⊢ ( ( ( ( 𝐴 ≠ ∅ ∧ ( 𝐴 ⊆ ℕ0s ∧ 𝐴 ∈ Fin ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 𝑦 ≤s 𝑥 ) ) ∧ 𝑧 ∈ 𝐴 ) → 𝑧 ∈ 𝐴 )
56 53 54 55 rspcdva ⊢ ( ( ( ( 𝐴 ≠ ∅ ∧ ( 𝐴 ⊆ ℕ0s ∧ 𝐴 ∈ Fin ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 𝑦 ≤s 𝑥 ) ) ∧ 𝑧 ∈ 𝐴 ) → 𝑧 ≤s 𝑥 )
57 51 34 syl ⊢ ( ( ( ( 𝐴 ≠ ∅ ∧ ( 𝐴 ⊆ ℕ0s ∧ 𝐴 ∈ Fin ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 𝑦 ≤s 𝑥 ) ) ∧ 𝑧 ∈ 𝐴 ) → 𝑥 ≤s 𝑥 )
58 breq2 ⊢ ( 𝑧 = 𝑥 → ( 𝑥 ≤s 𝑧 ↔ 𝑥 ≤s 𝑥 ) )
59 37 58 rexsn ⊢ ( ∃ 𝑧 ∈ { 𝑥 } 𝑥 ≤s 𝑧 ↔ 𝑥 ≤s 𝑥 )
60 57 59 sylibr ⊢ ( ( ( ( 𝐴 ≠ ∅ ∧ ( 𝐴 ⊆ ℕ0s ∧ 𝐴 ∈ Fin ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 𝑦 ≤s 𝑥 ) ) ∧ 𝑧 ∈ 𝐴 ) → ∃ 𝑧 ∈ { 𝑥 } 𝑥 ≤s 𝑧 )
61 60 orcd ⊢ ( ( ( ( 𝐴 ≠ ∅ ∧ ( 𝐴 ⊆ ℕ0s ∧ 𝐴 ∈ Fin ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 𝑦 ≤s 𝑥 ) ) ∧ 𝑧 ∈ 𝐴 ) → ( ∃ 𝑧 ∈ { 𝑥 } 𝑥 ≤s 𝑧 ∨ ∃ 𝑤 ∈ ( R ‘ 𝑥 ) 𝑤 ≤s ( { 𝑥 } |s ∅ ) ) )
62 lltropt ⊢ ( L ‘ 𝑥 ) <<s ( R ‘ 𝑥 )
63 62 a1i ⊢ ( ( ( ( 𝐴 ≠ ∅ ∧ ( 𝐴 ⊆ ℕ0s ∧ 𝐴 ∈ Fin ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 𝑦 ≤s 𝑥 ) ) ∧ 𝑧 ∈ 𝐴 ) → ( L ‘ 𝑥 ) <<s ( R ‘ 𝑥 ) )
64 31 adantr ⊢ ( ( ( ( 𝐴 ≠ ∅ ∧ ( 𝐴 ⊆ ℕ0s ∧ 𝐴 ∈ Fin ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 𝑦 ≤s 𝑥 ) ) ∧ 𝑧 ∈ 𝐴 ) → { 𝑥 } <<s ∅ )
65 lrcut ⊢ ( 𝑥 ∈ No → ( ( L ‘ 𝑥 ) |s ( R ‘ 𝑥 ) ) = 𝑥 )
66 51 65 syl ⊢ ( ( ( ( 𝐴 ≠ ∅ ∧ ( 𝐴 ⊆ ℕ0s ∧ 𝐴 ∈ Fin ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 𝑦 ≤s 𝑥 ) ) ∧ 𝑧 ∈ 𝐴 ) → ( ( L ‘ 𝑥 ) |s ( R ‘ 𝑥 ) ) = 𝑥 )
67 66 eqcomd ⊢ ( ( ( ( 𝐴 ≠ ∅ ∧ ( 𝐴 ⊆ ℕ0s ∧ 𝐴 ∈ Fin ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 𝑦 ≤s 𝑥 ) ) ∧ 𝑧 ∈ 𝐴 ) → 𝑥 = ( ( L ‘ 𝑥 ) |s ( R ‘ 𝑥 ) ) )
68 eqidd ⊢ ( ( ( ( 𝐴 ≠ ∅ ∧ ( 𝐴 ⊆ ℕ0s ∧ 𝐴 ∈ Fin ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 𝑦 ≤s 𝑥 ) ) ∧ 𝑧 ∈ 𝐴 ) → ( { 𝑥 } |s ∅ ) = ( { 𝑥 } |s ∅ ) )
69 sltrec ⊢ ( ( ( ( L ‘ 𝑥 ) <<s ( R ‘ 𝑥 ) ∧ { 𝑥 } <<s ∅ ) ∧ ( 𝑥 = ( ( L ‘ 𝑥 ) |s ( R ‘ 𝑥 ) ) ∧ ( { 𝑥 } |s ∅ ) = ( { 𝑥 } |s ∅ ) ) ) → ( 𝑥 <s ( { 𝑥 } |s ∅ ) ↔ ( ∃ 𝑧 ∈ { 𝑥 } 𝑥 ≤s 𝑧 ∨ ∃ 𝑤 ∈ ( R ‘ 𝑥 ) 𝑤 ≤s ( { 𝑥 } |s ∅ ) ) ) )
70 63 64 67 68 69 syl22anc ⊢ ( ( ( ( 𝐴 ≠ ∅ ∧ ( 𝐴 ⊆ ℕ0s ∧ 𝐴 ∈ Fin ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 𝑦 ≤s 𝑥 ) ) ∧ 𝑧 ∈ 𝐴 ) → ( 𝑥 <s ( { 𝑥 } |s ∅ ) ↔ ( ∃ 𝑧 ∈ { 𝑥 } 𝑥 ≤s 𝑧 ∨ ∃ 𝑤 ∈ ( R ‘ 𝑥 ) 𝑤 ≤s ( { 𝑥 } |s ∅ ) ) ) )
71 61 70 mpbird ⊢ ( ( ( ( 𝐴 ≠ ∅ ∧ ( 𝐴 ⊆ ℕ0s ∧ 𝐴 ∈ Fin ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 𝑦 ≤s 𝑥 ) ) ∧ 𝑧 ∈ 𝐴 ) → 𝑥 <s ( { 𝑥 } |s ∅ ) )
72 50 51 52 56 71 slelttrd ⊢ ( ( ( ( 𝐴 ≠ ∅ ∧ ( 𝐴 ⊆ ℕ0s ∧ 𝐴 ∈ Fin ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 𝑦 ≤s 𝑥 ) ) ∧ 𝑧 ∈ 𝐴 ) → 𝑧 <s ( { 𝑥 } |s ∅ ) )
73 velsn ⊢ ( 𝑤 ∈ { ( { 𝑥 } |s ∅ ) } ↔ 𝑤 = ( { 𝑥 } |s ∅ ) )
74 breq2 ⊢ ( 𝑤 = ( { 𝑥 } |s ∅ ) → ( 𝑧 <s 𝑤 ↔ 𝑧 <s ( { 𝑥 } |s ∅ ) ) )
75 73 74 sylbi ⊢ ( 𝑤 ∈ { ( { 𝑥 } |s ∅ ) } → ( 𝑧 <s 𝑤 ↔ 𝑧 <s ( { 𝑥 } |s ∅ ) ) )
76 72 75 syl5ibrcom ⊢ ( ( ( ( 𝐴 ≠ ∅ ∧ ( 𝐴 ⊆ ℕ0s ∧ 𝐴 ∈ Fin ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 𝑦 ≤s 𝑥 ) ) ∧ 𝑧 ∈ 𝐴 ) → ( 𝑤 ∈ { ( { 𝑥 } |s ∅ ) } → 𝑧 <s 𝑤 ) )
77 76 3impia ⊢ ( ( ( ( 𝐴 ≠ ∅ ∧ ( 𝐴 ⊆ ℕ0s ∧ 𝐴 ∈ Fin ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 𝑦 ≤s 𝑥 ) ) ∧ 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ { ( { 𝑥 } |s ∅ ) } ) → 𝑧 <s 𝑤 )
78 44 46 47 49 77 ssltd ⊢ ( ( ( 𝐴 ≠ ∅ ∧ ( 𝐴 ⊆ ℕ0s ∧ 𝐴 ∈ Fin ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 𝑦 ≤s 𝑥 ) ) → 𝐴 <<s { ( { 𝑥 } |s ∅ ) } )
79 snelpwi ⊢ ( ( { 𝑥 } |s ∅ ) ∈ No → { ( { 𝑥 } |s ∅ ) } ∈ 𝒫 No )
80 nulssgt ⊢ ( { ( { 𝑥 } |s ∅ ) } ∈ 𝒫 No → { ( { 𝑥 } |s ∅ ) } <<s ∅ )
81 48 79 80 3syl ⊢ ( ( ( 𝐴 ≠ ∅ ∧ ( 𝐴 ⊆ ℕ0s ∧ 𝐴 ∈ Fin ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 𝑦 ≤s 𝑥 ) ) → { ( { 𝑥 } |s ∅ ) } <<s ∅ )
82 31 41 43 78 81 cofcut1d ⊢ ( ( ( 𝐴 ≠ ∅ ∧ ( 𝐴 ⊆ ℕ0s ∧ 𝐴 ∈ Fin ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 𝑦 ≤s 𝑥 ) ) → ( { 𝑥 } |s ∅ ) = ( 𝐴 |s ∅ ) )
83 82 eqcomd ⊢ ( ( ( 𝐴 ≠ ∅ ∧ ( 𝐴 ⊆ ℕ0s ∧ 𝐴 ∈ Fin ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 𝑦 ≤s 𝑥 ) ) → ( 𝐴 |s ∅ ) = ( { 𝑥 } |s ∅ ) )
84 simplrl ⊢ ( ( ( 𝐴 ≠ ∅ ∧ ( 𝐴 ⊆ ℕ0s ∧ 𝐴 ∈ Fin ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 𝑦 ≤s 𝑥 ) ) → 𝐴 ⊆ ℕ0s )
85 84 33 sseldd ⊢ ( ( ( 𝐴 ≠ ∅ ∧ ( 𝐴 ⊆ ℕ0s ∧ 𝐴 ∈ Fin ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 𝑦 ≤s 𝑥 ) ) → 𝑥 ∈ ℕ0s )
86 peano2n0s ⊢ ( 𝑥 ∈ ℕ0s → ( 𝑥 +s 1s ) ∈ ℕ0s )
87 85 86 syl ⊢ ( ( ( 𝐴 ≠ ∅ ∧ ( 𝐴 ⊆ ℕ0s ∧ 𝐴 ∈ Fin ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 𝑦 ≤s 𝑥 ) ) → ( 𝑥 +s 1s ) ∈ ℕ0s )
88 n0scut ⊢ ( ( 𝑥 +s 1s ) ∈ ℕ0s → ( 𝑥 +s 1s ) = ( { ( ( 𝑥 +s 1s ) -s 1s ) } |s ∅ ) )
89 87 88 syl ⊢ ( ( ( 𝐴 ≠ ∅ ∧ ( 𝐴 ⊆ ℕ0s ∧ 𝐴 ∈ Fin ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 𝑦 ≤s 𝑥 ) ) → ( 𝑥 +s 1s ) = ( { ( ( 𝑥 +s 1s ) -s 1s ) } |s ∅ ) )
90 1sno ⊢ 1s ∈ No
91 pncans ⊢ ( ( 𝑥 ∈ No ∧ 1s ∈ No ) → ( ( 𝑥 +s 1s ) -s 1s ) = 𝑥 )
92 28 90 91 sylancl ⊢ ( ( ( 𝐴 ≠ ∅ ∧ ( 𝐴 ⊆ ℕ0s ∧ 𝐴 ∈ Fin ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 𝑦 ≤s 𝑥 ) ) → ( ( 𝑥 +s 1s ) -s 1s ) = 𝑥 )
93 92 sneqd ⊢ ( ( ( 𝐴 ≠ ∅ ∧ ( 𝐴 ⊆ ℕ0s ∧ 𝐴 ∈ Fin ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 𝑦 ≤s 𝑥 ) ) → { ( ( 𝑥 +s 1s ) -s 1s ) } = { 𝑥 } )
94 93 oveq1d ⊢ ( ( ( 𝐴 ≠ ∅ ∧ ( 𝐴 ⊆ ℕ0s ∧ 𝐴 ∈ Fin ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 𝑦 ≤s 𝑥 ) ) → ( { ( ( 𝑥 +s 1s ) -s 1s ) } |s ∅ ) = ( { 𝑥 } |s ∅ ) )
95 89 94 eqtr2d ⊢ ( ( ( 𝐴 ≠ ∅ ∧ ( 𝐴 ⊆ ℕ0s ∧ 𝐴 ∈ Fin ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 𝑦 ≤s 𝑥 ) ) → ( { 𝑥 } |s ∅ ) = ( 𝑥 +s 1s ) )
96 95 87 eqeltrd ⊢ ( ( ( 𝐴 ≠ ∅ ∧ ( 𝐴 ⊆ ℕ0s ∧ 𝐴 ∈ Fin ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 𝑦 ≤s 𝑥 ) ) → ( { 𝑥 } |s ∅ ) ∈ ℕ0s )
97 83 96 eqeltrd ⊢ ( ( ( 𝐴 ≠ ∅ ∧ ( 𝐴 ⊆ ℕ0s ∧ 𝐴 ∈ Fin ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 𝑦 ≤s 𝑥 ) ) → ( 𝐴 |s ∅ ) ∈ ℕ0s )
98 97 expr ⊢ ( ( ( 𝐴 ≠ ∅ ∧ ( 𝐴 ⊆ ℕ0s ∧ 𝐴 ∈ Fin ) ) ∧ 𝑥 ∈ 𝐴 ) → ( ∀ 𝑦 ∈ 𝐴 𝑦 ≤s 𝑥 → ( 𝐴 |s ∅ ) ∈ ℕ0s ) )
99 25 98 sylbird ⊢ ( ( ( 𝐴 ≠ ∅ ∧ ( 𝐴 ⊆ ℕ0s ∧ 𝐴 ∈ Fin ) ) ∧ 𝑥 ∈ 𝐴 ) → ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 → ( 𝐴 |s ∅ ) ∈ ℕ0s ) )
100 99 rexlimdva ⊢ ( ( 𝐴 ≠ ∅ ∧ ( 𝐴 ⊆ ℕ0s ∧ 𝐴 ∈ Fin ) ) → ( ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 → ( 𝐴 |s ∅ ) ∈ ℕ0s ) )
101 17 100 mpd ⊢ ( ( 𝐴 ≠ ∅ ∧ ( 𝐴 ⊆ ℕ0s ∧ 𝐴 ∈ Fin ) ) → ( 𝐴 |s ∅ ) ∈ ℕ0s )
102 101 ex ⊢ ( 𝐴 ≠ ∅ → ( ( 𝐴 ⊆ ℕ0s ∧ 𝐴 ∈ Fin ) → ( 𝐴 |s ∅ ) ∈ ℕ0s ) )
103 6 102 pm2.61ine ⊢ ( ( 𝐴 ⊆ ℕ0s ∧ 𝐴 ∈ Fin ) → ( 𝐴 |s ∅ ) ∈ ℕ0s )