oncutlt

Description: A surreal ordinal is the simplest number greater than all previous surreal ordinals. Theorem 15 of Conway p. 28. (Contributed by Scott Fenton, 4-Nov-2025)

		Ref	Expression
	Assertion	oncutlt	$⊢ A \in {On}_{s} \to A = \{x \in {On}_{s} \| x <_{s} A\} \|_{s} \emptyset$

Proof

Step	Hyp	Ref	Expression
1		onno	$⊢ A \in {On}_{s} \to A \in No$
2		ltonsex	$⊢ A \in No \to \{x \in {On}_{s} \| x <_{s} A\} \in V$
3	1 2	syl	$⊢ A \in {On}_{s} \to \{x \in {On}_{s} \| x <_{s} A\} \in V$
4		snexg	$⊢ A \in {On}_{s} \to \{A\} \in V$
5		ssrab2	$⊢ \{x \in {On}_{s} \| x <_{s} A\} \subseteq {On}_{s}$
6		onssno	$⊢ {On}_{s} \subseteq No$
7	5 6	sstri	$⊢ \{x \in {On}_{s} \| x <_{s} A\} \subseteq No$
8	7	a1i	$⊢ A \in {On}_{s} \to \{x \in {On}_{s} \| x <_{s} A\} \subseteq No$
9	1	snssd	$⊢ A \in {On}_{s} \to \{A\} \subseteq No$
10		breq1	$⊢ x = y \to (x <_{s} A \leftrightarrow y <_{s} A)$
11	10	elrab	$⊢ y \in \{x \in {On}_{s} \| x <_{s} A\} \leftrightarrow (y \in {On}_{s} \land y <_{s} A)$
12	11	simprbi	$⊢ y \in \{x \in {On}_{s} \| x <_{s} A\} \to y <_{s} A$
13		velsn	$⊢ z \in \{A\} \leftrightarrow z = A$
14		breq2	$⊢ z = A \to (y <_{s} z \leftrightarrow y <_{s} A)$
15	13 14	sylbi	$⊢ z \in \{A\} \to (y <_{s} z \leftrightarrow y <_{s} A)$
16	12 15	syl5ibrcom	$⊢ y \in \{x \in {On}_{s} \| x <_{s} A\} \to (z \in \{A\} \to y <_{s} z)$
17	16	imp	$⊢ (y \in \{x \in {On}_{s} \| x <_{s} A\} \land z \in \{A\}) \to y <_{s} z$
18	17	3adant1	$⊢ (A \in {On}_{s} \land y \in \{x \in {On}_{s} \| x <_{s} A\} \land z \in \{A\}) \to y <_{s} z$
19	3 4 8 9 18	sltsd	$⊢ A \in {On}_{s} \to \{x \in {On}_{s} \| x <_{s} A\} ≪_{s} \{A\}$
20		snelpwi	$⊢ A \in No \to \{A\} \in 𝒫 No$
21		nulsgts	$⊢ \{A\} \in 𝒫 No \to \{A\} ≪_{s} \emptyset$
22	1 20 21	3syl	$⊢ A \in {On}_{s} \to \{A\} ≪_{s} \emptyset$
23		sltssep	$⊢ \{x \in {On}_{s} \| x <_{s} A\} ≪_{s} \{y\} \to \forall z \in \{x \in {On}_{s} \| x <_{s} A\} \forall w \in \{y\} z <_{s} w$
24		vex	$⊢ y \in V$
25		breq2	$⊢ w = y \to (z <_{s} w \leftrightarrow z <_{s} y)$
26	24 25	ralsn	$⊢ \forall w \in \{y\} z <_{s} w \leftrightarrow z <_{s} y$
27	26	ralbii	$⊢ \forall z \in \{x \in {On}_{s} \| x <_{s} A\} \forall w \in \{y\} z <_{s} w \leftrightarrow \forall z \in \{x \in {On}_{s} \| x <_{s} A\} z <_{s} y$
28		breq1	$⊢ x = z \to (x <_{s} A \leftrightarrow z <_{s} A)$
29	28	ralrab	$⊢ \forall z \in \{x \in {On}_{s} \| x <_{s} A\} z <_{s} y \leftrightarrow \forall z \in {On}_{s} (z <_{s} A \to z <_{s} y)$
30	27 29	bitri	$⊢ \forall z \in \{x \in {On}_{s} \| x <_{s} A\} \forall w \in \{y\} z <_{s} w \leftrightarrow \forall z \in {On}_{s} (z <_{s} A \to z <_{s} y)$
31	23 30	sylib	$⊢ \{x \in {On}_{s} \| x <_{s} A\} ≪_{s} \{y\} \to \forall z \in {On}_{s} (z <_{s} A \to z <_{s} y)$
32		fvex	$⊢ L (y) \in V$
33		fvex	$⊢ R (y) \in V$
34	32 33	unex	$⊢ L (y) \cup R (y) \in V$
35	34	a1i	$⊢ ((A \in {On}_{s} \land y \in No) \land bday (y) \in bday (A)) \to L (y) \cup R (y) \in V$
36		leftssno	$⊢ L (y) \subseteq No$
37		rightssno	$⊢ R (y) \subseteq No$
38	36 37	unssi	$⊢ L (y) \cup R (y) \subseteq No$
39	38	a1i	$⊢ ((A \in {On}_{s} \land y \in No) \land bday (y) \in bday (A)) \to L (y) \cup R (y) \subseteq No$
40		eqidd	$⊢ ((A \in {On}_{s} \land y \in No) \land bday (y) \in bday (A)) \to (L (y) \cup R (y)) \|_{s} \emptyset = (L (y) \cup R (y)) \|_{s} \emptyset$
41	35 39 40	elons2d	$⊢ ((A \in {On}_{s} \land y \in No) \land bday (y) \in bday (A)) \to (L (y) \cup R (y)) \|_{s} \emptyset \in {On}_{s}$
42	34	elpw	$⊢ L (y) \cup R (y) \in 𝒫 No \leftrightarrow L (y) \cup R (y) \subseteq No$
43	38 42	mpbir	$⊢ L (y) \cup R (y) \in 𝒫 No$
44		nulsgts	$⊢ L (y) \cup R (y) \in 𝒫 No \to (L (y) \cup R (y)) ≪_{s} \emptyset$
45	43 44	mp1i	$⊢ ((A \in {On}_{s} \land y \in No) \land bday (y) \in bday (A)) \to (L (y) \cup R (y)) ≪_{s} \emptyset$
46		un0	$⊢ (L (y) \cup R (y)) \cup \emptyset = L (y) \cup R (y)$
47		lrold	$⊢ L (y) \cup R (y) = Old (bday (y))$
48	46 47	eqtri	$⊢ (L (y) \cup R (y)) \cup \emptyset = Old (bday (y))$
49	48	imaeq2i	$⊢ bday [(L (y) \cup R (y)) \cup \emptyset] = bday [Old (bday (y))]$
50		simpr	$⊢ (((A \in {On}_{s} \land y \in No) \land bday (y) \in bday (A)) \land z \in Old (bday (y))) \to z \in Old (bday (y))$
51		bdayon	$⊢ bday (y) \in On$
52		oldssno	$⊢ Old (bday (y)) \subseteq No$
53	52	sseli	$⊢ z \in Old (bday (y)) \to z \in No$
54	53	adantl	$⊢ (((A \in {On}_{s} \land y \in No) \land bday (y) \in bday (A)) \land z \in Old (bday (y))) \to z \in No$
55		oldbday	$⊢ (bday (y) \in On \land z \in No) \to (z \in Old (bday (y)) \leftrightarrow bday (z) \in bday (y))$
56	51 54 55	sylancr	$⊢ (((A \in {On}_{s} \land y \in No) \land bday (y) \in bday (A)) \land z \in Old (bday (y))) \to (z \in Old (bday (y)) \leftrightarrow bday (z) \in bday (y))$
57	50 56	mpbid	$⊢ (((A \in {On}_{s} \land y \in No) \land bday (y) \in bday (A)) \land z \in Old (bday (y))) \to bday (z) \in bday (y)$
58	57	ralrimiva	$⊢ ((A \in {On}_{s} \land y \in No) \land bday (y) \in bday (A)) \to \forall z \in Old (bday (y)) bday (z) \in bday (y)$
59		bdayfun	$⊢ Fun bday$
60		bdaydm	$⊢ dom bday = No$
61	52 60	sseqtrri	$⊢ Old (bday (y)) \subseteq dom bday$
62		funimass4	$⊢ (Fun bday \land Old (bday (y)) \subseteq dom bday) \to (bday [Old (bday (y))] \subseteq bday (y) \leftrightarrow \forall z \in Old (bday (y)) bday (z) \in bday (y))$
63	59 61 62	mp2an	$⊢ bday [Old (bday (y))] \subseteq bday (y) \leftrightarrow \forall z \in Old (bday (y)) bday (z) \in bday (y)$
64	58 63	sylibr	$⊢ ((A \in {On}_{s} \land y \in No) \land bday (y) \in bday (A)) \to bday [Old (bday (y))] \subseteq bday (y)$
65	49 64	eqsstrid	$⊢ ((A \in {On}_{s} \land y \in No) \land bday (y) \in bday (A)) \to bday [(L (y) \cup R (y)) \cup \emptyset] \subseteq bday (y)$
66		cutbdaybnd	$⊢ ((L (y) \cup R (y)) ≪_{s} \emptyset \land bday (y) \in On \land bday [(L (y) \cup R (y)) \cup \emptyset] \subseteq bday (y)) \to bday ((L (y) \cup R (y)) \|_{s} \emptyset) \subseteq bday (y)$
67	51 66	mp3an2	$⊢ ((L (y) \cup R (y)) ≪_{s} \emptyset \land bday [(L (y) \cup R (y)) \cup \emptyset] \subseteq bday (y)) \to bday ((L (y) \cup R (y)) \|_{s} \emptyset) \subseteq bday (y)$
68	45 65 67	syl2anc	$⊢ ((A \in {On}_{s} \land y \in No) \land bday (y) \in bday (A)) \to bday ((L (y) \cup R (y)) \|_{s} \emptyset) \subseteq bday (y)$
69		simpr	$⊢ ((A \in {On}_{s} \land y \in No) \land bday (y) \in bday (A)) \to bday (y) \in bday (A)$
70		bdayon	$⊢ bday ((L (y) \cup R (y)) \|_{s} \emptyset) \in On$
71		bdayon	$⊢ bday (A) \in On$
72		ontr2	$⊢ (bday ((L (y) \cup R (y)) \|_{s} \emptyset) \in On \land bday (A) \in On) \to ((bday ((L (y) \cup R (y)) \|_{s} \emptyset) \subseteq bday (y) \land bday (y) \in bday (A)) \to bday ((L (y) \cup R (y)) \|_{s} \emptyset) \in bday (A))$
73	70 71 72	mp2an	$⊢ (bday ((L (y) \cup R (y)) \|_{s} \emptyset) \subseteq bday (y) \land bday (y) \in bday (A)) \to bday ((L (y) \cup R (y)) \|_{s} \emptyset) \in bday (A)$
74	68 69 73	syl2anc	$⊢ ((A \in {On}_{s} \land y \in No) \land bday (y) \in bday (A)) \to bday ((L (y) \cup R (y)) \|_{s} \emptyset) \in bday (A)$
75	45	cutscld	$⊢ ((A \in {On}_{s} \land y \in No) \land bday (y) \in bday (A)) \to (L (y) \cup R (y)) \|_{s} \emptyset \in No$
76		oldbday	$⊢ (bday (A) \in On \land (L (y) \cup R (y)) \|_{s} \emptyset \in No) \to ((L (y) \cup R (y)) \|_{s} \emptyset \in Old (bday (A)) \leftrightarrow bday ((L (y) \cup R (y)) \|_{s} \emptyset) \in bday (A))$
77	71 75 76	sylancr	$⊢ ((A \in {On}_{s} \land y \in No) \land bday (y) \in bday (A)) \to ((L (y) \cup R (y)) \|_{s} \emptyset \in Old (bday (A)) \leftrightarrow bday ((L (y) \cup R (y)) \|_{s} \emptyset) \in bday (A))$
78	74 77	mpbird	$⊢ ((A \in {On}_{s} \land y \in No) \land bday (y) \in bday (A)) \to (L (y) \cup R (y)) \|_{s} \emptyset \in Old (bday (A))$
79		elons	$⊢ A \in {On}_{s} \leftrightarrow (A \in No \land R (A) = \emptyset)$
80	79	simprbi	$⊢ A \in {On}_{s} \to R (A) = \emptyset$
81	80	ad2antrr	$⊢ ((A \in {On}_{s} \land y \in No) \land bday (y) \in bday (A)) \to R (A) = \emptyset$
82	81	uneq2d	$⊢ ((A \in {On}_{s} \land y \in No) \land bday (y) \in bday (A)) \to L (A) \cup R (A) = L (A) \cup \emptyset$
83		lrold	$⊢ L (A) \cup R (A) = Old (bday (A))$
84		un0	$⊢ L (A) \cup \emptyset = L (A)$
85	82 83 84	3eqtr3g	$⊢ ((A \in {On}_{s} \land y \in No) \land bday (y) \in bday (A)) \to Old (bday (A)) = L (A)$
86	78 85	eleqtrd	$⊢ ((A \in {On}_{s} \land y \in No) \land bday (y) \in bday (A)) \to (L (y) \cup R (y)) \|_{s} \emptyset \in L (A)$
87		leftlt	$⊢ (L (y) \cup R (y)) \|_{s} \emptyset \in L (A) \to ((L (y) \cup R (y)) \|_{s} \emptyset) <_{s} A$
88	86 87	syl	$⊢ ((A \in {On}_{s} \land y \in No) \land bday (y) \in bday (A)) \to ((L (y) \cup R (y)) \|_{s} \emptyset) <_{s} A$
89		simplr	$⊢ ((A \in {On}_{s} \land y \in No) \land bday (y) \in bday (A)) \to y \in No$
90		lesid	$⊢ y \in No \to y \leq_{s} y$
91		lrcut	$⊢ y \in No \to L (y) \|_{s} R (y) = y$
92	90 91	breqtrrd	$⊢ y \in No \to y \leq_{s} (L (y) \|_{s} R (y))$
93	89 92	syl	$⊢ ((A \in {On}_{s} \land y \in No) \land bday (y) \in bday (A)) \to y \leq_{s} (L (y) \|_{s} R (y))$
94		uneq2	$⊢ R (y) = \emptyset \to L (y) \cup R (y) = L (y) \cup \emptyset$
95		un0	$⊢ L (y) \cup \emptyset = L (y)$
96	94 95	eqtrdi	$⊢ R (y) = \emptyset \to L (y) \cup R (y) = L (y)$
97		eqcom	$⊢ R (y) = \emptyset \leftrightarrow \emptyset = R (y)$
98	97	biimpi	$⊢ R (y) = \emptyset \to \emptyset = R (y)$
99	96 98	oveq12d	$⊢ R (y) = \emptyset \to (L (y) \cup R (y)) \|_{s} \emptyset = L (y) \|_{s} R (y)$
100	99	breq2d	$⊢ R (y) = \emptyset \to (y \leq_{s} ((L (y) \cup R (y)) \|_{s} \emptyset) \leftrightarrow y \leq_{s} (L (y) \|_{s} R (y)))$
101	93 100	imbitrrid	$⊢ R (y) = \emptyset \to (((A \in {On}_{s} \land y \in No) \land bday (y) \in bday (A)) \to y \leq_{s} ((L (y) \cup R (y)) \|_{s} \emptyset))$
102		simprlr	$⊢ (R (y) \neq \emptyset \land ((A \in {On}_{s} \land y \in No) \land bday (y) \in bday (A))) \to y \in No$
103	75	adantl	$⊢ (R (y) \neq \emptyset \land ((A \in {On}_{s} \land y \in No) \land bday (y) \in bday (A))) \to (L (y) \cup R (y)) \|_{s} \emptyset \in No$
104		n0	$⊢ R (y) \neq \emptyset \leftrightarrow \exists w w \in R (y)$
105		breq2	$⊢ z = w \to (y \leq_{s} z \leftrightarrow y \leq_{s} w)$
106		elun2	$⊢ w \in R (y) \to w \in (L (y) \cup R (y))$
107	106	adantr	$⊢ (w \in R (y) \land ((A \in {On}_{s} \land y \in No) \land bday (y) \in bday (A))) \to w \in (L (y) \cup R (y))$
108		simprlr	$⊢ (w \in R (y) \land ((A \in {On}_{s} \land y \in No) \land bday (y) \in bday (A))) \to y \in No$
109	37	sseli	$⊢ w \in R (y) \to w \in No$
110	109	adantr	$⊢ (w \in R (y) \land ((A \in {On}_{s} \land y \in No) \land bday (y) \in bday (A))) \to w \in No$
111		rightgt	$⊢ w \in R (y) \to y <_{s} w$
112	111	adantr	$⊢ (w \in R (y) \land ((A \in {On}_{s} \land y \in No) \land bday (y) \in bday (A))) \to y <_{s} w$
113	108 110 112	ltlesd	$⊢ (w \in R (y) \land ((A \in {On}_{s} \land y \in No) \land bday (y) \in bday (A))) \to y \leq_{s} w$
114	105 107 113	rspcedvdw	$⊢ (w \in R (y) \land ((A \in {On}_{s} \land y \in No) \land bday (y) \in bday (A))) \to \exists z \in (L (y) \cup R (y)) y \leq_{s} z$
115	114	ex	$⊢ w \in R (y) \to (((A \in {On}_{s} \land y \in No) \land bday (y) \in bday (A)) \to \exists z \in (L (y) \cup R (y)) y \leq_{s} z)$
116	115	exlimiv	$⊢ \exists w w \in R (y) \to (((A \in {On}_{s} \land y \in No) \land bday (y) \in bday (A)) \to \exists z \in (L (y) \cup R (y)) y \leq_{s} z)$
117	104 116	sylbi	$⊢ R (y) \neq \emptyset \to (((A \in {On}_{s} \land y \in No) \land bday (y) \in bday (A)) \to \exists z \in (L (y) \cup R (y)) y \leq_{s} z)$
118	117	imp	$⊢ (R (y) \neq \emptyset \land ((A \in {On}_{s} \land y \in No) \land bday (y) \in bday (A))) \to \exists z \in (L (y) \cup R (y)) y \leq_{s} z$
119	118	orcd	$⊢ (R (y) \neq \emptyset \land ((A \in {On}_{s} \land y \in No) \land bday (y) \in bday (A))) \to (\exists z \in (L (y) \cup R (y)) y \leq_{s} z \lor \exists w \in R (y) w \leq_{s} ((L (y) \cup R (y)) \|_{s} \emptyset))$
120		lltr	$⊢ L (y) ≪_{s} R (y)$
121	120	a1i	$⊢ (R (y) \neq \emptyset \land ((A \in {On}_{s} \land y \in No) \land bday (y) \in bday (A))) \to L (y) ≪_{s} R (y)$
122	43 44	mp1i	$⊢ (R (y) \neq \emptyset \land ((A \in {On}_{s} \land y \in No) \land bday (y) \in bday (A))) \to (L (y) \cup R (y)) ≪_{s} \emptyset$
123	102 91	syl	$⊢ (R (y) \neq \emptyset \land ((A \in {On}_{s} \land y \in No) \land bday (y) \in bday (A))) \to L (y) \|_{s} R (y) = y$
124	123	eqcomd	$⊢ (R (y) \neq \emptyset \land ((A \in {On}_{s} \land y \in No) \land bday (y) \in bday (A))) \to y = L (y) \|_{s} R (y)$
125		eqidd	$⊢ (R (y) \neq \emptyset \land ((A \in {On}_{s} \land y \in No) \land bday (y) \in bday (A))) \to (L (y) \cup R (y)) \|_{s} \emptyset = (L (y) \cup R (y)) \|_{s} \emptyset$
126	121 122 124 125	ltsrecd	$⊢ (R (y) \neq \emptyset \land ((A \in {On}_{s} \land y \in No) \land bday (y) \in bday (A))) \to (y <_{s} ((L (y) \cup R (y)) \|_{s} \emptyset) \leftrightarrow (\exists z \in (L (y) \cup R (y)) y \leq_{s} z \lor \exists w \in R (y) w \leq_{s} ((L (y) \cup R (y)) \|_{s} \emptyset)))$
127	119 126	mpbird	$⊢ (R (y) \neq \emptyset \land ((A \in {On}_{s} \land y \in No) \land bday (y) \in bday (A))) \to y <_{s} ((L (y) \cup R (y)) \|_{s} \emptyset)$
128	102 103 127	ltlesd	$⊢ (R (y) \neq \emptyset \land ((A \in {On}_{s} \land y \in No) \land bday (y) \in bday (A))) \to y \leq_{s} ((L (y) \cup R (y)) \|_{s} \emptyset)$
129	128	ex	$⊢ R (y) \neq \emptyset \to (((A \in {On}_{s} \land y \in No) \land bday (y) \in bday (A)) \to y \leq_{s} ((L (y) \cup R (y)) \|_{s} \emptyset))$
130	101 129	pm2.61ine	$⊢ ((A \in {On}_{s} \land y \in No) \land bday (y) \in bday (A)) \to y \leq_{s} ((L (y) \cup R (y)) \|_{s} \emptyset)$
131		lenlts	$⊢ (y \in No \land (L (y) \cup R (y)) \|_{s} \emptyset \in No) \to (y \leq_{s} ((L (y) \cup R (y)) \|_{s} \emptyset) \leftrightarrow \neg ((L (y) \cup R (y)) \|_{s} \emptyset) <_{s} y)$
132	89 75 131	syl2anc	$⊢ ((A \in {On}_{s} \land y \in No) \land bday (y) \in bday (A)) \to (y \leq_{s} ((L (y) \cup R (y)) \|_{s} \emptyset) \leftrightarrow \neg ((L (y) \cup R (y)) \|_{s} \emptyset) <_{s} y)$
133	130 132	mpbid	$⊢ ((A \in {On}_{s} \land y \in No) \land bday (y) \in bday (A)) \to \neg ((L (y) \cup R (y)) \|_{s} \emptyset) <_{s} y$
134		breq1	$⊢ z = (L (y) \cup R (y)) \|_{s} \emptyset \to (z <_{s} A \leftrightarrow ((L (y) \cup R (y)) \|_{s} \emptyset) <_{s} A)$
135		breq1	$⊢ z = (L (y) \cup R (y)) \|_{s} \emptyset \to (z <_{s} y \leftrightarrow ((L (y) \cup R (y)) \|_{s} \emptyset) <_{s} y)$
136	135	notbid	$⊢ z = (L (y) \cup R (y)) \|_{s} \emptyset \to (\neg z <_{s} y \leftrightarrow \neg ((L (y) \cup R (y)) \|_{s} \emptyset) <_{s} y)$
137	134 136	anbi12d	$⊢ z = (L (y) \cup R (y)) \|_{s} \emptyset \to ((z <_{s} A \land \neg z <_{s} y) \leftrightarrow (((L (y) \cup R (y)) \|_{s} \emptyset) <_{s} A \land \neg ((L (y) \cup R (y)) \|_{s} \emptyset) <_{s} y))$
138	137	rspcev	$⊢ ((L (y) \cup R (y)) \|_{s} \emptyset \in {On}_{s} \land (((L (y) \cup R (y)) \|_{s} \emptyset) <_{s} A \land \neg ((L (y) \cup R (y)) \|_{s} \emptyset) <_{s} y)) \to \exists z \in {On}_{s} (z <_{s} A \land \neg z <_{s} y)$
139	41 88 133 138	syl12anc	$⊢ ((A \in {On}_{s} \land y \in No) \land bday (y) \in bday (A)) \to \exists z \in {On}_{s} (z <_{s} A \land \neg z <_{s} y)$
140	139	ex	$⊢ (A \in {On}_{s} \land y \in No) \to (bday (y) \in bday (A) \to \exists z \in {On}_{s} (z <_{s} A \land \neg z <_{s} y))$
141		ontri1	$⊢ (bday (A) \in On \land bday (y) \in On) \to (bday (A) \subseteq bday (y) \leftrightarrow \neg bday (y) \in bday (A))$
142	71 51 141	mp2an	$⊢ bday (A) \subseteq bday (y) \leftrightarrow \neg bday (y) \in bday (A)$
143	142	con2bii	$⊢ bday (y) \in bday (A) \leftrightarrow \neg bday (A) \subseteq bday (y)$
144		rexanali	$⊢ \exists z \in {On}_{s} (z <_{s} A \land \neg z <_{s} y) \leftrightarrow \neg \forall z \in {On}_{s} (z <_{s} A \to z <_{s} y)$
145	140 143 144	3imtr3g	$⊢ (A \in {On}_{s} \land y \in No) \to (\neg bday (A) \subseteq bday (y) \to \neg \forall z \in {On}_{s} (z <_{s} A \to z <_{s} y))$
146	145	con4d	$⊢ (A \in {On}_{s} \land y \in No) \to (\forall z \in {On}_{s} (z <_{s} A \to z <_{s} y) \to bday (A) \subseteq bday (y))$
147	31 146	syl5	$⊢ (A \in {On}_{s} \land y \in No) \to (\{x \in {On}_{s} \| x <_{s} A\} ≪_{s} \{y\} \to bday (A) \subseteq bday (y))$
148	147	adantrd	$⊢ (A \in {On}_{s} \land y \in No) \to ((\{x \in {On}_{s} \| x <_{s} A\} ≪_{s} \{y\} \land \{y\} ≪_{s} \emptyset) \to bday (A) \subseteq bday (y))$
149	148	ralrimiva	$⊢ A \in {On}_{s} \to \forall y \in No ((\{x \in {On}_{s} \| x <_{s} A\} ≪_{s} \{y\} \land \{y\} ≪_{s} \emptyset) \to bday (A) \subseteq bday (y))$
150	3 8	elpwd	$⊢ A \in {On}_{s} \to \{x \in {On}_{s} \| x <_{s} A\} \in 𝒫 No$
151		nulsgts	$⊢ \{x \in {On}_{s} \| x <_{s} A\} \in 𝒫 No \to \{x \in {On}_{s} \| x <_{s} A\} ≪_{s} \emptyset$
152	150 151	syl	$⊢ A \in {On}_{s} \to \{x \in {On}_{s} \| x <_{s} A\} ≪_{s} \emptyset$
153		eqcuts2	$⊢ (\{x \in {On}_{s} \| x <_{s} A\} ≪_{s} \emptyset \land A \in No) \to (\{x \in {On}_{s} \| x <_{s} A\} \|_{s} \emptyset = A \leftrightarrow (\{x \in {On}_{s} \| x <_{s} A\} ≪_{s} \{A\} \land \{A\} ≪_{s} \emptyset \land \forall y \in No ((\{x \in {On}_{s} \| x <_{s} A\} ≪_{s} \{y\} \land \{y\} ≪_{s} \emptyset) \to bday (A) \subseteq bday (y))))$
154	152 1 153	syl2anc	$⊢ A \in {On}_{s} \to (\{x \in {On}_{s} \| x <_{s} A\} \|_{s} \emptyset = A \leftrightarrow (\{x \in {On}_{s} \| x <_{s} A\} ≪_{s} \{A\} \land \{A\} ≪_{s} \emptyset \land \forall y \in No ((\{x \in {On}_{s} \| x <_{s} A\} ≪_{s} \{y\} \land \{y\} ≪_{s} \emptyset) \to bday (A) \subseteq bday (y))))$
155	19 22 149 154	mpbir3and	$⊢ A \in {On}_{s} \to \{x \in {On}_{s} \| x <_{s} A\} \|_{s} \emptyset = A$
156	155	eqcomd	$⊢ A \in {On}_{s} \to A = \{x \in {On}_{s} \| x <_{s} A\} \|_{s} \emptyset$

Metamath Proof Explorer

Theorem oncutlt

Proof