Metamath Proof Explorer

Theorem n0fincut

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 n0fincut ( ( 𝐴 ⊆ ℕ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 ltsso ⊢ <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 lenlts ⊢ ( ( 𝑦 ∈ 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 nulsgts ⊢ ( { 𝑥 } ∈ 𝒫 No → { 𝑥 } <<s ∅ )
31 28 29 30 3syl ⊢ ( ( ( 𝐴 ≠ ∅ ∧ ( 𝐴 ⊆ ℕ0s ∧ 𝐴 ∈ Fin ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 𝑦 ≤s 𝑥 ) ) → { 𝑥 } <<s ∅ )
32 breq2 ⊢ ( 𝑤 = 𝑥 → ( 𝑥 ≤s 𝑤 ↔ 𝑥 ≤s 𝑥 ) )
33 simprl ⊢ ( ( ( 𝐴 ≠ ∅ ∧ ( 𝐴 ⊆ ℕ0s ∧ 𝐴 ∈ Fin ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 𝑦 ≤s 𝑥 ) ) → 𝑥 ∈ 𝐴 )
34 lesid ⊢ ( 𝑥 ∈ 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 cutscld ⊢ ( ( ( 𝐴 ≠ ∅ ∧ ( 𝐴 ⊆ ℕ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 lltr ⊢ ( 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 63 64 67 68 ltsrecd ⊢ ( ( ( ( 𝐴 ≠ ∅ ∧ ( 𝐴 ⊆ ℕ0s ∧ 𝐴 ∈ Fin ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 𝑦 ≤s 𝑥 ) ) ∧ 𝑧 ∈ 𝐴 ) → ( 𝑥 <s ( { 𝑥 } |s ∅ ) ↔ ( ∃ 𝑧 ∈ { 𝑥 } 𝑥 ≤s 𝑧 ∨ ∃ 𝑤 ∈ ( R ‘ 𝑥 ) 𝑤 ≤s ( { 𝑥 } |s ∅ ) ) ) )
70 61 69 mpbird ⊢ ( ( ( ( 𝐴 ≠ ∅ ∧ ( 𝐴 ⊆ ℕ0s ∧ 𝐴 ∈ Fin ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 𝑦 ≤s 𝑥 ) ) ∧ 𝑧 ∈ 𝐴 ) → 𝑥 <s ( { 𝑥 } |s ∅ ) )
71 50 51 52 56 70 leltstrd ⊢ ( ( ( ( 𝐴 ≠ ∅ ∧ ( 𝐴 ⊆ ℕ0s ∧ 𝐴 ∈ Fin ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 𝑦 ≤s 𝑥 ) ) ∧ 𝑧 ∈ 𝐴 ) → 𝑧 <s ( { 𝑥 } |s ∅ ) )
72 velsn ⊢ ( 𝑤 ∈ { ( { 𝑥 } |s ∅ ) } ↔ 𝑤 = ( { 𝑥 } |s ∅ ) )
73 breq2 ⊢ ( 𝑤 = ( { 𝑥 } |s ∅ ) → ( 𝑧 <s 𝑤 ↔ 𝑧 <s ( { 𝑥 } |s ∅ ) ) )
74 72 73 sylbi ⊢ ( 𝑤 ∈ { ( { 𝑥 } |s ∅ ) } → ( 𝑧 <s 𝑤 ↔ 𝑧 <s ( { 𝑥 } |s ∅ ) ) )
75 71 74 syl5ibrcom ⊢ ( ( ( ( 𝐴 ≠ ∅ ∧ ( 𝐴 ⊆ ℕ0s ∧ 𝐴 ∈ Fin ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 𝑦 ≤s 𝑥 ) ) ∧ 𝑧 ∈ 𝐴 ) → ( 𝑤 ∈ { ( { 𝑥 } |s ∅ ) } → 𝑧 <s 𝑤 ) )
76 75 3impia ⊢ ( ( ( ( 𝐴 ≠ ∅ ∧ ( 𝐴 ⊆ ℕ0s ∧ 𝐴 ∈ Fin ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 𝑦 ≤s 𝑥 ) ) ∧ 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ { ( { 𝑥 } |s ∅ ) } ) → 𝑧 <s 𝑤 )
77 44 46 47 49 76 sltsd ⊢ ( ( ( 𝐴 ≠ ∅ ∧ ( 𝐴 ⊆ ℕ0s ∧ 𝐴 ∈ Fin ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 𝑦 ≤s 𝑥 ) ) → 𝐴 <<s { ( { 𝑥 } |s ∅ ) } )
78 snelpwi ⊢ ( ( { 𝑥 } |s ∅ ) ∈ No → { ( { 𝑥 } |s ∅ ) } ∈ 𝒫 No )
79 nulsgts ⊢ ( { ( { 𝑥 } |s ∅ ) } ∈ 𝒫 No → { ( { 𝑥 } |s ∅ ) } <<s ∅ )
80 48 78 79 3syl ⊢ ( ( ( 𝐴 ≠ ∅ ∧ ( 𝐴 ⊆ ℕ0s ∧ 𝐴 ∈ Fin ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 𝑦 ≤s 𝑥 ) ) → { ( { 𝑥 } |s ∅ ) } <<s ∅ )
81 31 41 43 77 80 cofcut1d ⊢ ( ( ( 𝐴 ≠ ∅ ∧ ( 𝐴 ⊆ ℕ0s ∧ 𝐴 ∈ Fin ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 𝑦 ≤s 𝑥 ) ) → ( { 𝑥 } |s ∅ ) = ( 𝐴 |s ∅ ) )
82 81 eqcomd ⊢ ( ( ( 𝐴 ≠ ∅ ∧ ( 𝐴 ⊆ ℕ0s ∧ 𝐴 ∈ Fin ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 𝑦 ≤s 𝑥 ) ) → ( 𝐴 |s ∅ ) = ( { 𝑥 } |s ∅ ) )
83 simplrl ⊢ ( ( ( 𝐴 ≠ ∅ ∧ ( 𝐴 ⊆ ℕ0s ∧ 𝐴 ∈ Fin ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 𝑦 ≤s 𝑥 ) ) → 𝐴 ⊆ ℕ0s )
84 83 33 sseldd ⊢ ( ( ( 𝐴 ≠ ∅ ∧ ( 𝐴 ⊆ ℕ0s ∧ 𝐴 ∈ Fin ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 𝑦 ≤s 𝑥 ) ) → 𝑥 ∈ ℕ0s )
85 84 peano2n0sd ⊢ ( ( ( 𝐴 ≠ ∅ ∧ ( 𝐴 ⊆ ℕ0s ∧ 𝐴 ∈ Fin ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 𝑦 ≤s 𝑥 ) ) → ( 𝑥 +s 1s ) ∈ ℕ0s )
86 n0cut ⊢ ( ( 𝑥 +s 1s ) ∈ ℕ0s → ( 𝑥 +s 1s ) = ( { ( ( 𝑥 +s 1s ) -s 1s ) } |s ∅ ) )
87 85 86 syl ⊢ ( ( ( 𝐴 ≠ ∅ ∧ ( 𝐴 ⊆ ℕ0s ∧ 𝐴 ∈ Fin ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 𝑦 ≤s 𝑥 ) ) → ( 𝑥 +s 1s ) = ( { ( ( 𝑥 +s 1s ) -s 1s ) } |s ∅ ) )
88 1no ⊢ 1s ∈ No
89 pncans ⊢ ( ( 𝑥 ∈ No ∧ 1s ∈ No ) → ( ( 𝑥 +s 1s ) -s 1s ) = 𝑥 )
90 28 88 89 sylancl ⊢ ( ( ( 𝐴 ≠ ∅ ∧ ( 𝐴 ⊆ ℕ0s ∧ 𝐴 ∈ Fin ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 𝑦 ≤s 𝑥 ) ) → ( ( 𝑥 +s 1s ) -s 1s ) = 𝑥 )
91 90 sneqd ⊢ ( ( ( 𝐴 ≠ ∅ ∧ ( 𝐴 ⊆ ℕ0s ∧ 𝐴 ∈ Fin ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 𝑦 ≤s 𝑥 ) ) → { ( ( 𝑥 +s 1s ) -s 1s ) } = { 𝑥 } )
92 91 oveq1d ⊢ ( ( ( 𝐴 ≠ ∅ ∧ ( 𝐴 ⊆ ℕ0s ∧ 𝐴 ∈ Fin ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 𝑦 ≤s 𝑥 ) ) → ( { ( ( 𝑥 +s 1s ) -s 1s ) } |s ∅ ) = ( { 𝑥 } |s ∅ ) )
93 87 92 eqtr2d ⊢ ( ( ( 𝐴 ≠ ∅ ∧ ( 𝐴 ⊆ ℕ0s ∧ 𝐴 ∈ Fin ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 𝑦 ≤s 𝑥 ) ) → ( { 𝑥 } |s ∅ ) = ( 𝑥 +s 1s ) )
94 93 85 eqeltrd ⊢ ( ( ( 𝐴 ≠ ∅ ∧ ( 𝐴 ⊆ ℕ0s ∧ 𝐴 ∈ Fin ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 𝑦 ≤s 𝑥 ) ) → ( { 𝑥 } |s ∅ ) ∈ ℕ0s )
95 82 94 eqeltrd ⊢ ( ( ( 𝐴 ≠ ∅ ∧ ( 𝐴 ⊆ ℕ0s ∧ 𝐴 ∈ Fin ) ) ∧ ( 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 𝑦 ≤s 𝑥 ) ) → ( 𝐴 |s ∅ ) ∈ ℕ0s )
96 95 expr ⊢ ( ( ( 𝐴 ≠ ∅ ∧ ( 𝐴 ⊆ ℕ0s ∧ 𝐴 ∈ Fin ) ) ∧ 𝑥 ∈ 𝐴 ) → ( ∀ 𝑦 ∈ 𝐴 𝑦 ≤s 𝑥 → ( 𝐴 |s ∅ ) ∈ ℕ0s ) )
97 25 96 sylbird ⊢ ( ( ( 𝐴 ≠ ∅ ∧ ( 𝐴 ⊆ ℕ0s ∧ 𝐴 ∈ Fin ) ) ∧ 𝑥 ∈ 𝐴 ) → ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 → ( 𝐴 |s ∅ ) ∈ ℕ0s ) )
98 97 rexlimdva ⊢ ( ( 𝐴 ≠ ∅ ∧ ( 𝐴 ⊆ ℕ0s ∧ 𝐴 ∈ Fin ) ) → ( ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 → ( 𝐴 |s ∅ ) ∈ ℕ0s ) )
99 17 98 mpd ⊢ ( ( 𝐴 ≠ ∅ ∧ ( 𝐴 ⊆ ℕ0s ∧ 𝐴 ∈ Fin ) ) → ( 𝐴 |s ∅ ) ∈ ℕ0s )
100 99 ex ⊢ ( 𝐴 ≠ ∅ → ( ( 𝐴 ⊆ ℕ0s ∧ 𝐴 ∈ Fin ) → ( 𝐴 |s ∅ ) ∈ ℕ0s ) )
101 6 100 pm2.61ine ⊢ ( ( 𝐴 ⊆ ℕ0s ∧ 𝐴 ∈ Fin ) → ( 𝐴 |s ∅ ) ∈ ℕ0s )