Theorem exmidunben 13037

Description: If any unbounded set of positive integers is equinumerous to NN, then the Limited Principle of Omniscience (LPO) implies excluded middle. (Contributed by Jim Kingdon, 29-Jul-2023.)

Assertion

Ref	Expression
exmidunben	|- ( ( A. x ( ( x C_ NN /\ A. m e. NN E. n e. x m < n ) -> x ~~ NN ) /\ om e. Omni ) -> EXMID )

Distinct variable group:   m, n, x

Proof of Theorem exmidunben

Dummy variables f y z w are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		vex 2803	. . . . . . . . . . 11 |- y e. _V
2	1	enref 6933	. . . . . . . . . 10 |- y ~~ y
3		2z 9497	. . . . . . . . . . 11 |- 2 e. ZZ
4		uzennn 10688	. . . . . . . . . . 11 |- ( 2 e. ZZ -> ( ZZ>= ` 2 ) ~~ NN )
5	3, 4	ax-mp 5	. . . . . . . . . 10 |- ( ZZ>= ` 2 ) ~~ NN
6		djuen 7416	. . . . . . . . . 10 |- ( ( y ~~ y /\ ( ZZ>= ` 2 ) ~~ NN ) -> ( y ⊔ ( ZZ>= ` 2 ) ) ~~ ( y ⊔ NN ) )
7	2, 5, 6	mp2an 426	. . . . . . . . 9 |- ( y ⊔ ( ZZ>= ` 2 ) ) ~~ ( y ⊔ NN )
8	7	ensymi 6951	. . . . . . . 8 |- ( y ⊔ NN ) ~~ ( y ⊔ ( ZZ>= ` 2 ) )
9		zex 9478	. . . . . . . . . . 11 |- ZZ e. _V
10		uzssz 9766	. . . . . . . . . . 11 |- ( ZZ>= ` 2 ) C_ ZZ
11	9, 10	ssexi 4225	. . . . . . . . . 10 |- ( ZZ>= ` 2 ) e. _V
12		1re 8168	. . . . . . . . . . . . . . 15 |- 1 e. RR
13	12	ltnri 8262	. . . . . . . . . . . . . 14 |- -. 1 < 1
14		simplr 528	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( A. x ( ( x C_ NN /\ A. m e. NN E. n e. x m < n ) -> x ~~ NN ) /\ om e. Omni ) /\ y C_ { 1 } ) /\ z e. y ) -> y C_ { 1 } )
15		simpr 110	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( A. x ( ( x C_ NN /\ A. m e. NN E. n e. x m < n ) -> x ~~ NN ) /\ om e. Omni ) /\ y C_ { 1 } ) /\ z e. y ) -> z e. y )
16	14, 15	sseldd 3226	. . . . . . . . . . . . . . . 16 |- ( ( ( ( A. x ( ( x C_ NN /\ A. m e. NN E. n e. x m < n ) -> x ~~ NN ) /\ om e. Omni ) /\ y C_ { 1 } ) /\ z e. y ) -> z e. { 1 } )
17		elsni 3685	. . . . . . . . . . . . . . . 16 |- ( z e. { 1 } -> z = 1 )
18	16, 17	syl 14	. . . . . . . . . . . . . . 15 |- ( ( ( ( A. x ( ( x C_ NN /\ A. m e. NN E. n e. x m < n ) -> x ~~ NN ) /\ om e. Omni ) /\ y C_ { 1 } ) /\ z e. y ) -> z = 1 )
19	18	breq2d 4098	. . . . . . . . . . . . . 14 |- ( ( ( ( A. x ( ( x C_ NN /\ A. m e. NN E. n e. x m < n ) -> x ~~ NN ) /\ om e. Omni ) /\ y C_ { 1 } ) /\ z e. y ) -> ( 1 < z <-> 1 < 1 ) )
20	13, 19	mtbiri 679	. . . . . . . . . . . . 13 |- ( ( ( ( A. x ( ( x C_ NN /\ A. m e. NN E. n e. x m < n ) -> x ~~ NN ) /\ om e. Omni ) /\ y C_ { 1 } ) /\ z e. y ) -> -. 1 < z )
21		eluz2gt1 9826	. . . . . . . . . . . . 13 |- ( z e. ( ZZ>= ` 2 ) -> 1 < z )
22	20, 21	nsyl 631	. . . . . . . . . . . 12 |- ( ( ( ( A. x ( ( x C_ NN /\ A. m e. NN E. n e. x m < n ) -> x ~~ NN ) /\ om e. Omni ) /\ y C_ { 1 } ) /\ z e. y ) -> -. z e. ( ZZ>= ` 2 ) )
23	22	ralrimiva 2603	. . . . . . . . . . 11 |- ( ( ( A. x ( ( x C_ NN /\ A. m e. NN E. n e. x m < n ) -> x ~~ NN ) /\ om e. Omni ) /\ y C_ { 1 } ) -> A. z e. y -. z e. ( ZZ>= ` 2 ) )
24		disj 3541	. . . . . . . . . . 11 |- ( ( y i^i ( ZZ>= ` 2 ) ) = (/) <-> A. z e. y -. z e. ( ZZ>= ` 2 ) )
25	23, 24	sylibr 134	. . . . . . . . . 10 |- ( ( ( A. x ( ( x C_ NN /\ A. m e. NN E. n e. x m < n ) -> x ~~ NN ) /\ om e. Omni ) /\ y C_ { 1 } ) -> ( y i^i ( ZZ>= ` 2 ) ) = (/) )
26		endjudisj 7415	. . . . . . . . . 10 |- ( ( y e. _V /\ ( ZZ>= ` 2 ) e. _V /\ ( y i^i ( ZZ>= ` 2 ) ) = (/) ) -> ( y ⊔ ( ZZ>= ` 2 ) ) ~~ ( y u. ( ZZ>= ` 2 ) ) )
27	1, 11, 25, 26	mp3an12i 1375	. . . . . . . . 9 |- ( ( ( A. x ( ( x C_ NN /\ A. m e. NN E. n e. x m < n ) -> x ~~ NN ) /\ om e. Omni ) /\ y C_ { 1 } ) -> ( y ⊔ ( ZZ>= ` 2 ) ) ~~ ( y u. ( ZZ>= ` 2 ) ) )
28		simpr 110	. . . . . . . . . . . 12 |- ( ( ( A. x ( ( x C_ NN /\ A. m e. NN E. n e. x m < n ) -> x ~~ NN ) /\ om e. Omni ) /\ y C_ { 1 } ) -> y C_ { 1 } )
29		1nn 9144	. . . . . . . . . . . . 13 |- 1 e. NN
30		snssi 3815	. . . . . . . . . . . . 13 |- ( 1 e. NN -> { 1 } C_ NN )
31	29, 30	ax-mp 5	. . . . . . . . . . . 12 |- { 1 } C_ NN
32	28, 31	sstrdi 3237	. . . . . . . . . . 11 |- ( ( ( A. x ( ( x C_ NN /\ A. m e. NN E. n e. x m < n ) -> x ~~ NN ) /\ om e. Omni ) /\ y C_ { 1 } ) -> y C_ NN )
33		2nn 9295	. . . . . . . . . . . 12 |- 2 e. NN
34		uznnssnn 9801	. . . . . . . . . . . 12 |- ( 2 e. NN -> ( ZZ>= ` 2 ) C_ NN )
35	33, 34	mp1i 10	. . . . . . . . . . 11 |- ( ( ( A. x ( ( x C_ NN /\ A. m e. NN E. n e. x m < n ) -> x ~~ NN ) /\ om e. Omni ) /\ y C_ { 1 } ) -> ( ZZ>= ` 2 ) C_ NN )
36	32, 35	unssd 3381	. . . . . . . . . 10 |- ( ( ( A. x ( ( x C_ NN /\ A. m e. NN E. n e. x m < n ) -> x ~~ NN ) /\ om e. Omni ) /\ y C_ { 1 } ) -> ( y u. ( ZZ>= ` 2 ) ) C_ NN )
37		nfv 1574	. . . . . . . . . . . . . . . 16 |- F/ m x C_ NN
38		nfra1 2561	. . . . . . . . . . . . . . . 16 |- F/ m A. m e. NN E. n e. x m < n
39	37, 38	nfan 1611	. . . . . . . . . . . . . . 15 |- F/ m ( x C_ NN /\ A. m e. NN E. n e. x m < n )
40		nfv 1574	. . . . . . . . . . . . . . 15 |- F/ m x ~~ NN
41	39, 40	nfim 1618	. . . . . . . . . . . . . 14 |- F/ m ( ( x C_ NN /\ A. m e. NN E. n e. x m < n ) -> x ~~ NN )
42	41	nfal 1622	. . . . . . . . . . . . 13 |- F/ m A. x ( ( x C_ NN /\ A. m e. NN E. n e. x m < n ) -> x ~~ NN )
43		nfv 1574	. . . . . . . . . . . . 13 |- F/ m om e. Omni
44	42, 43	nfan 1611	. . . . . . . . . . . 12 |- F/ m ( A. x ( ( x C_ NN /\ A. m e. NN E. n e. x m < n ) -> x ~~ NN ) /\ om e. Omni )
45		nfv 1574	. . . . . . . . . . . 12 |- F/ m y C_ { 1 }
46	44, 45	nfan 1611	. . . . . . . . . . 11 |- F/ m ( ( A. x ( ( x C_ NN /\ A. m e. NN E. n e. x m < n ) -> x ~~ NN ) /\ om e. Omni ) /\ y C_ { 1 } )
47		simpr 110	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( A. x ( ( x C_ NN /\ A. m e. NN E. n e. x m < n ) -> x ~~ NN ) /\ om e. Omni ) /\ y C_ { 1 } ) /\ m e. NN ) -> m e. NN )
48	47	peano2nnd 9148	. . . . . . . . . . . . . . . 16 |- ( ( ( ( A. x ( ( x C_ NN /\ A. m e. NN E. n e. x m < n ) -> x ~~ NN ) /\ om e. Omni ) /\ y C_ { 1 } ) /\ m e. NN ) -> ( m + 1 ) e. NN )
49	48	nnzd 9591	. . . . . . . . . . . . . . 15 |- ( ( ( ( A. x ( ( x C_ NN /\ A. m e. NN E. n e. x m < n ) -> x ~~ NN ) /\ om e. Omni ) /\ y C_ { 1 } ) /\ m e. NN ) -> ( m + 1 ) e. ZZ )
50		0p1e1 9247	. . . . . . . . . . . . . . . . 17 |- ( 0 + 1 ) = 1
51		0red 8170	. . . . . . . . . . . . . . . . . 18 |- ( m e. NN -> 0 e. RR )
52		nnre 9140	. . . . . . . . . . . . . . . . . 18 |- ( m e. NN -> m e. RR )
53		1red 8184	. . . . . . . . . . . . . . . . . 18 |- ( m e. NN -> 1 e. RR )
54		nngt0 9158	. . . . . . . . . . . . . . . . . 18 |- ( m e. NN -> 0 < m )
55	51, 52, 53, 54	ltadd1dd 8726	. . . . . . . . . . . . . . . . 17 |- ( m e. NN -> ( 0 + 1 ) < ( m + 1 ) )
56	50, 55	eqbrtrrid 4122	. . . . . . . . . . . . . . . 16 |- ( m e. NN -> 1 < ( m + 1 ) )
57	56	adantl 277	. . . . . . . . . . . . . . 15 |- ( ( ( ( A. x ( ( x C_ NN /\ A. m e. NN E. n e. x m < n ) -> x ~~ NN ) /\ om e. Omni ) /\ y C_ { 1 } ) /\ m e. NN ) -> 1 < ( m + 1 ) )
58		eluz2b1 9825	. . . . . . . . . . . . . . 15 |- ( ( m + 1 ) e. ( ZZ>= ` 2 ) <-> ( ( m + 1 ) e. ZZ /\ 1 < ( m + 1 ) ) )
59	49, 57, 58	sylanbrc 417	. . . . . . . . . . . . . 14 |- ( ( ( ( A. x ( ( x C_ NN /\ A. m e. NN E. n e. x m < n ) -> x ~~ NN ) /\ om e. Omni ) /\ y C_ { 1 } ) /\ m e. NN ) -> ( m + 1 ) e. ( ZZ>= ` 2 ) )
60		elun2 3373	. . . . . . . . . . . . . 14 |- ( ( m + 1 ) e. ( ZZ>= ` 2 ) -> ( m + 1 ) e. ( y u. ( ZZ>= ` 2 ) ) )
61	59, 60	syl 14	. . . . . . . . . . . . 13 |- ( ( ( ( A. x ( ( x C_ NN /\ A. m e. NN E. n e. x m < n ) -> x ~~ NN ) /\ om e. Omni ) /\ y C_ { 1 } ) /\ m e. NN ) -> ( m + 1 ) e. ( y u. ( ZZ>= ` 2 ) ) )
62	47	nnred 9146	. . . . . . . . . . . . . 14 |- ( ( ( ( A. x ( ( x C_ NN /\ A. m e. NN E. n e. x m < n ) -> x ~~ NN ) /\ om e. Omni ) /\ y C_ { 1 } ) /\ m e. NN ) -> m e. RR )
63	62	ltp1d 9100	. . . . . . . . . . . . 13 |- ( ( ( ( A. x ( ( x C_ NN /\ A. m e. NN E. n e. x m < n ) -> x ~~ NN ) /\ om e. Omni ) /\ y C_ { 1 } ) /\ m e. NN ) -> m < ( m + 1 ) )
64		breq2 4090	. . . . . . . . . . . . . 14 |- ( n = ( m + 1 ) -> ( m < n <-> m < ( m + 1 ) ) )
65	64	rspcev 2908	. . . . . . . . . . . . 13 |- ( ( ( m + 1 ) e. ( y u. ( ZZ>= ` 2 ) ) /\ m < ( m + 1 ) ) -> E. n e. ( y u. ( ZZ>= ` 2 ) ) m < n )
66	61, 63, 65	syl2anc 411	. . . . . . . . . . . 12 |- ( ( ( ( A. x ( ( x C_ NN /\ A. m e. NN E. n e. x m < n ) -> x ~~ NN ) /\ om e. Omni ) /\ y C_ { 1 } ) /\ m e. NN ) -> E. n e. ( y u. ( ZZ>= ` 2 ) ) m < n )
67	66	ex 115	. . . . . . . . . . 11 |- ( ( ( A. x ( ( x C_ NN /\ A. m e. NN E. n e. x m < n ) -> x ~~ NN ) /\ om e. Omni ) /\ y C_ { 1 } ) -> ( m e. NN -> E. n e. ( y u. ( ZZ>= ` 2 ) ) m < n ) )
68	46, 67	ralrimi 2601	. . . . . . . . . 10 |- ( ( ( A. x ( ( x C_ NN /\ A. m e. NN E. n e. x m < n ) -> x ~~ NN ) /\ om e. Omni ) /\ y C_ { 1 } ) -> A. m e. NN E. n e. ( y u. ( ZZ>= ` 2 ) ) m < n )
69	1, 11	unex 4536	. . . . . . . . . . . 12 |- ( y u. ( ZZ>= ` 2 ) ) e. _V
70		sseq1 3248	. . . . . . . . . . . . . 14 |- ( x = ( y u. ( ZZ>= ` 2 ) ) -> ( x C_ NN <-> ( y u. ( ZZ>= ` 2 ) ) C_ NN ) )
71		rexeq 2729	. . . . . . . . . . . . . . 15 |- ( x = ( y u. ( ZZ>= ` 2 ) ) -> ( E. n e. x m < n <-> E. n e. ( y u. ( ZZ>= ` 2 ) ) m < n ) )
72	71	ralbidv 2530	. . . . . . . . . . . . . 14 |- ( x = ( y u. ( ZZ>= ` 2 ) ) -> ( A. m e. NN E. n e. x m < n <-> A. m e. NN E. n e. ( y u. ( ZZ>= ` 2 ) ) m < n ) )
73	70, 72	anbi12d 473	. . . . . . . . . . . . 13 |- ( x = ( y u. ( ZZ>= ` 2 ) ) -> ( ( x C_ NN /\ A. m e. NN E. n e. x m < n ) <-> ( ( y u. ( ZZ>= ` 2 ) ) C_ NN /\ A. m e. NN E. n e. ( y u. ( ZZ>= ` 2 ) ) m < n ) ) )
74		breq1 4089	. . . . . . . . . . . . 13 |- ( x = ( y u. ( ZZ>= ` 2 ) ) -> ( x ~~ NN <-> ( y u. ( ZZ>= ` 2 ) ) ~~ NN ) )
75	73, 74	imbi12d 234	. . . . . . . . . . . 12 |- ( x = ( y u. ( ZZ>= ` 2 ) ) -> ( ( ( x C_ NN /\ A. m e. NN E. n e. x m < n ) -> x ~~ NN ) <-> ( ( ( y u. ( ZZ>= ` 2 ) ) C_ NN /\ A. m e. NN E. n e. ( y u. ( ZZ>= ` 2 ) ) m < n ) -> ( y u. ( ZZ>= ` 2 ) ) ~~ NN ) ) )
76	69, 75	spcv 2898	. . . . . . . . . . 11 |- ( A. x ( ( x C_ NN /\ A. m e. NN E. n e. x m < n ) -> x ~~ NN ) -> ( ( ( y u. ( ZZ>= ` 2 ) ) C_ NN /\ A. m e. NN E. n e. ( y u. ( ZZ>= ` 2 ) ) m < n ) -> ( y u. ( ZZ>= ` 2 ) ) ~~ NN ) )
77	76	ad2antrr 488	. . . . . . . . . 10 |- ( ( ( A. x ( ( x C_ NN /\ A. m e. NN E. n e. x m < n ) -> x ~~ NN ) /\ om e. Omni ) /\ y C_ { 1 } ) -> ( ( ( y u. ( ZZ>= ` 2 ) ) C_ NN /\ A. m e. NN E. n e. ( y u. ( ZZ>= ` 2 ) ) m < n ) -> ( y u. ( ZZ>= ` 2 ) ) ~~ NN ) )
78	36, 68, 77	mp2and 433	. . . . . . . . 9 |- ( ( ( A. x ( ( x C_ NN /\ A. m e. NN E. n e. x m < n ) -> x ~~ NN ) /\ om e. Omni ) /\ y C_ { 1 } ) -> ( y u. ( ZZ>= ` 2 ) ) ~~ NN )
79		entr 6953	. . . . . . . . 9 |- ( ( ( y ⊔ ( ZZ>= ` 2 ) ) ~~ ( y u. ( ZZ>= ` 2 ) ) /\ ( y u. ( ZZ>= ` 2 ) ) ~~ NN ) -> ( y ⊔ ( ZZ>= ` 2 ) ) ~~ NN )
80	27, 78, 79	syl2anc 411	. . . . . . . 8 |- ( ( ( A. x ( ( x C_ NN /\ A. m e. NN E. n e. x m < n ) -> x ~~ NN ) /\ om e. Omni ) /\ y C_ { 1 } ) -> ( y ⊔ ( ZZ>= ` 2 ) ) ~~ NN )
81		entr 6953	. . . . . . . 8 |- ( ( ( y ⊔ NN ) ~~ ( y ⊔ ( ZZ>= ` 2 ) ) /\ ( y ⊔ ( ZZ>= ` 2 ) ) ~~ NN ) -> ( y ⊔ NN ) ~~ NN )
82	8, 80, 81	sylancr 414	. . . . . . 7 |- ( ( ( A. x ( ( x C_ NN /\ A. m e. NN E. n e. x m < n ) -> x ~~ NN ) /\ om e. Omni ) /\ y C_ { 1 } ) -> ( y ⊔ NN ) ~~ NN )
83	82	ensymd 6952	. . . . . 6 |- ( ( ( A. x ( ( x C_ NN /\ A. m e. NN E. n e. x m < n ) -> x ~~ NN ) /\ om e. Omni ) /\ y C_ { 1 } ) -> NN ~~ ( y ⊔ NN ) )
84		bren 6912	. . . . . 6 |- ( NN ~~ ( y ⊔ NN ) <-> E. f f : NN -1-1-onto-> ( y ⊔ NN ) )
85	83, 84	sylib 122	. . . . 5 |- ( ( ( A. x ( ( x C_ NN /\ A. m e. NN E. n e. x m < n ) -> x ~~ NN ) /\ om e. Omni ) /\ y C_ { 1 } ) -> E. f f : NN -1-1-onto-> ( y ⊔ NN ) )
86		simpllr 534	. . . . . . . . 9 |- ( ( ( ( A. x ( ( x C_ NN /\ A. m e. NN E. n e. x m < n ) -> x ~~ NN ) /\ om e. Omni ) /\ y C_ { 1 } ) /\ f : NN -1-1-onto-> ( y ⊔ NN ) ) -> om e. Omni )
87		nnenom 10686	. . . . . . . . . 10 |- NN ~~ om
88		enomni 7329	. . . . . . . . . 10 |- ( NN ~~ om -> ( NN e. Omni <-> om e. Omni ) )
89	87, 88	ax-mp 5	. . . . . . . . 9 |- ( NN e. Omni <-> om e. Omni )
90	86, 89	sylibr 134	. . . . . . . 8 |- ( ( ( ( A. x ( ( x C_ NN /\ A. m e. NN E. n e. x m < n ) -> x ~~ NN ) /\ om e. Omni ) /\ y C_ { 1 } ) /\ f : NN -1-1-onto-> ( y ⊔ NN ) ) -> NN e. Omni )
91		f1ofo 5587	. . . . . . . . 9 |- ( f : NN -1-1-onto-> ( y ⊔ NN ) -> f : NN -onto-> ( y ⊔ NN ) )
92	91	adantl 277	. . . . . . . 8 |- ( ( ( ( A. x ( ( x C_ NN /\ A. m e. NN E. n e. x m < n ) -> x ~~ NN ) /\ om e. Omni ) /\ y C_ { 1 } ) /\ f : NN -1-1-onto-> ( y ⊔ NN ) ) -> f : NN -onto-> ( y ⊔ NN ) )
93	90, 92	fodjuomni 7339	. . . . . . 7 |- ( ( ( ( A. x ( ( x C_ NN /\ A. m e. NN E. n e. x m < n ) -> x ~~ NN ) /\ om e. Omni ) /\ y C_ { 1 } ) /\ f : NN -1-1-onto-> ( y ⊔ NN ) ) -> ( E. w w e. y \/ y = (/) ) )
94	93	orcomd 734	. . . . . 6 |- ( ( ( ( A. x ( ( x C_ NN /\ A. m e. NN E. n e. x m < n ) -> x ~~ NN ) /\ om e. Omni ) /\ y C_ { 1 } ) /\ f : NN -1-1-onto-> ( y ⊔ NN ) ) -> ( y = (/) \/ E. w w e. y ) )
95		simplr 528	. . . . . . . 8 |- ( ( ( ( A. x ( ( x C_ NN /\ A. m e. NN E. n e. x m < n ) -> x ~~ NN ) /\ om e. Omni ) /\ y C_ { 1 } ) /\ f : NN -1-1-onto-> ( y ⊔ NN ) ) -> y C_ { 1 } )
96		sssnm 3835	. . . . . . . 8 |- ( E. w w e. y -> ( y C_ { 1 } <-> y = { 1 } ) )
97	95, 96	syl5ibcom 155	. . . . . . 7 |- ( ( ( ( A. x ( ( x C_ NN /\ A. m e. NN E. n e. x m < n ) -> x ~~ NN ) /\ om e. Omni ) /\ y C_ { 1 } ) /\ f : NN -1-1-onto-> ( y ⊔ NN ) ) -> ( E. w w e. y -> y = { 1 } ) )
98	97	orim2d 793	. . . . . 6 |- ( ( ( ( A. x ( ( x C_ NN /\ A. m e. NN E. n e. x m < n ) -> x ~~ NN ) /\ om e. Omni ) /\ y C_ { 1 } ) /\ f : NN -1-1-onto-> ( y ⊔ NN ) ) -> ( ( y = (/) \/ E. w w e. y ) -> ( y = (/) \/ y = { 1 } ) ) )
99	94, 98	mpd 13	. . . . 5 |- ( ( ( ( A. x ( ( x C_ NN /\ A. m e. NN E. n e. x m < n ) -> x ~~ NN ) /\ om e. Omni ) /\ y C_ { 1 } ) /\ f : NN -1-1-onto-> ( y ⊔ NN ) ) -> ( y = (/) \/ y = { 1 } ) )
100	85, 99	exlimddv 1945	. . . 4 |- ( ( ( A. x ( ( x C_ NN /\ A. m e. NN E. n e. x m < n ) -> x ~~ NN ) /\ om e. Omni ) /\ y C_ { 1 } ) -> ( y = (/) \/ y = { 1 } ) )
101	100	ex 115	. . 3 |- ( ( A. x ( ( x C_ NN /\ A. m e. NN E. n e. x m < n ) -> x ~~ NN ) /\ om e. Omni ) -> ( y C_ { 1 } -> ( y = (/) \/ y = { 1 } ) ) )
102	101	alrimiv 1920	. 2 |- ( ( A. x ( ( x C_ NN /\ A. m e. NN E. n e. x m < n ) -> x ~~ NN ) /\ om e. Omni ) -> A. y ( y C_ { 1 } -> ( y = (/) \/ y = { 1 } ) ) )
103		exmidsssnc 4291	. . 3 |- ( 1 e. NN -> (EXMID <-> A. y ( y C_ { 1 } -> ( y = (/) \/ y = { 1 } ) ) ) )
104	29, 103	ax-mp 5	. 2 |- (EXMID <-> A. y ( y C_ { 1 } -> ( y = (/) \/ y = { 1 } ) ) )
105	102, 104	sylibr 134	1 |- ( ( A. x ( ( x C_ NN /\ A. m e. NN E. n e. x m < n ) -> x ~~ NN ) /\ om e. Omni ) -> EXMID )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 104   <-> wb 105   \/ wo 713   A.wal 1393   = wceq 1395   E.wex 1538   e. wcel 2200   A.wral 2508   E.wrex 2509   _Vcvv 2800   u. cun 3196   i^i cin 3197   C_ wss 3198   (/)c0 3492   {csn 3667   class class class wbr 4086  EXMIDwem 4282   omcom 4686   -onto->wfo 5322   -1-1-onto->wf1o 5323   ` cfv 5324  (class class class)co 6013   ~~ cen 6902   ⊔ cdju 7227  Omnicomni 7324   0cc0 8022   1c1 8023   + caddc 8025   < clt 8204   NNcn 9133   2c2 9184   ZZcz 9469   ZZ>=cuz 9745

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 617  ax-in2 618  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-13 2202  ax-14 2203  ax-ext 2211  ax-coll 4202  ax-sep 4205  ax-nul 4213  ax-pow 4262  ax-pr 4297  ax-un 4528  ax-setind 4633  ax-iinf 4684  ax-cnex 8113  ax-resscn 8114  ax-1cn 8115  ax-1re 8116  ax-icn 8117  ax-addcl 8118  ax-addrcl 8119  ax-mulcl 8120  ax-addcom 8122  ax-addass 8124  ax-distr 8126  ax-i2m1 8127  ax-0lt1 8128  ax-0id 8130  ax-rnegex 8131  ax-cnre 8133  ax-pre-ltirr 8134  ax-pre-ltwlin 8135  ax-pre-lttrn 8136  ax-pre-ltadd 8138

This theorem depends on definitions:  df-bi 117  df-dc 840  df-3or 1003  df-3an 1004  df-tru 1398  df-fal 1401  df-nf 1507  df-sb 1809  df-eu 2080  df-mo 2081  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ne 2401  df-nel 2496  df-ral 2513  df-rex 2514  df-reu 2515  df-rab 2517  df-v 2802  df-sbc 3030  df-csb 3126  df-dif 3200  df-un 3202  df-in 3204  df-ss 3211  df-nul 3493  df-if 3604  df-pw 3652  df-sn 3673  df-pr 3674  df-op 3676  df-uni 3892  df-int 3927  df-iun 3970  df-br 4087  df-opab 4149  df-mpt 4150  df-tr 4186  df-exmid 4283  df-id 4388  df-iord 4461  df-on 4463  df-ilim 4464  df-suc 4466  df-iom 4687  df-xp 4729  df-rel 4730  df-cnv 4731  df-co 4732  df-dm 4733  df-rn 4734  df-res 4735  df-ima 4736  df-iota 5284  df-fun 5326  df-fn 5327  df-f 5328  df-f1 5329  df-fo 5330  df-f1o 5331  df-fv 5332  df-riota 5966  df-ov 6016  df-oprab 6017  df-mpo 6018  df-1st 6298  df-2nd 6299  df-recs 6466  df-frec 6552  df-1o 6577  df-2o 6578  df-er 6697  df-map 6814  df-en 6905  df-dju 7228  df-inl 7237  df-inr 7238  df-omni 7325  df-pnf 8206  df-mnf 8207  df-xr 8208  df-ltxr 8209  df-le 8210  df-sub 8342  df-neg 8343  df-inn 9134  df-2 9192  df-n0 9393  df-z 9470  df-uz 9746

This theorem is referenced by: (None)