Theorem exmid1stab 13880

Description: If any proposition is stable, excluded middle follows. We are thinking of x as a proposition and x = { (/) } as "x is true". (Contributed by Jim Kingdon, 28-Nov-2023.)

Hypothesis

Ref	Expression
exmid1stab.x	|- ( ( ph /\ x C_ { (/) } ) -> STAB x = { (/) } )

Assertion

Ref	Expression
exmid1stab	|- ( ph -> EXMID )

Distinct variable group:   ph, x

Proof of Theorem exmid1stab

Dummy variable y is distinct from all other variables.

Step	Hyp	Ref	Expression
1		0ex 4109	. . . . . . . . 9 |- (/) e. _V
2	1	snid 3607	. . . . . . . 8 |- (/) e. { (/) }
3		nnexmid 840	. . . . . . . . . . 11 |- -. -. ( y = { (/) } \/ -. y = { (/) } )
4		uneq1 3269	. . . . . . . . . . . . . . 15 |- ( y = { (/) } -> ( y u. ( { (/) } \ y ) ) = ( { (/) } u. ( { (/) } \ y ) ) )
5		undifabs 3485	. . . . . . . . . . . . . . 15 |- ( { (/) } u. ( { (/) } \ y ) ) = { (/) }
6	4, 5	eqtrdi 2215	. . . . . . . . . . . . . 14 |- ( y = { (/) } -> ( y u. ( { (/) } \ y ) ) = { (/) } )
7	6	a1i 9	. . . . . . . . . . . . 13 |- ( y C_ { (/) } -> ( y = { (/) } -> ( y u. ( { (/) } \ y ) ) = { (/) } ) )
8		df-ne 2337	. . . . . . . . . . . . . . . . 17 |- ( y =/= { (/) } <-> -. y = { (/) } )
9		pwntru 4178	. . . . . . . . . . . . . . . . 17 |- ( ( y C_ { (/) } /\ y =/= { (/) } ) -> y = (/) )
10	8, 9	sylan2br 286	. . . . . . . . . . . . . . . 16 |- ( ( y C_ { (/) } /\ -. y = { (/) } ) -> y = (/) )
11	10	difeq2d 3240	. . . . . . . . . . . . . . . . 17 |- ( ( y C_ { (/) } /\ -. y = { (/) } ) -> ( { (/) } \ y ) = ( { (/) } \ (/) ) )
12		dif0 3479	. . . . . . . . . . . . . . . . 17 |- ( { (/) } \ (/) ) = { (/) }
13	11, 12	eqtrdi 2215	. . . . . . . . . . . . . . . 16 |- ( ( y C_ { (/) } /\ -. y = { (/) } ) -> ( { (/) } \ y ) = { (/) } )
14	10, 13	uneq12d 3277	. . . . . . . . . . . . . . 15 |- ( ( y C_ { (/) } /\ -. y = { (/) } ) -> ( y u. ( { (/) } \ y ) ) = ( (/) u. { (/) } ) )
15		uncom 3266	. . . . . . . . . . . . . . . 16 |- ( (/) u. { (/) } ) = ( { (/) } u. (/) )
16		un0 3442	. . . . . . . . . . . . . . . 16 |- ( { (/) } u. (/) ) = { (/) }
17	15, 16	eqtri 2186	. . . . . . . . . . . . . . 15 |- ( (/) u. { (/) } ) = { (/) }
18	14, 17	eqtrdi 2215	. . . . . . . . . . . . . 14 |- ( ( y C_ { (/) } /\ -. y = { (/) } ) -> ( y u. ( { (/) } \ y ) ) = { (/) } )
19	18	ex 114	. . . . . . . . . . . . 13 |- ( y C_ { (/) } -> ( -. y = { (/) } -> ( y u. ( { (/) } \ y ) ) = { (/) } ) )
20	7, 19	jaod 707	. . . . . . . . . . . 12 |- ( y C_ { (/) } -> ( ( y = { (/) } \/ -. y = { (/) } ) -> ( y u. ( { (/) } \ y ) ) = { (/) } ) )
21	20	con3d 621	. . . . . . . . . . 11 |- ( y C_ { (/) } -> ( -. ( y u. ( { (/) } \ y ) ) = { (/) } -> -. ( y = { (/) } \/ -. y = { (/) } ) ) )
22	3, 21	mtoi 654	. . . . . . . . . 10 |- ( y C_ { (/) } -> -. -. ( y u. ( { (/) } \ y ) ) = { (/) } )
23	22	adantl 275	. . . . . . . . 9 |- ( ( ph /\ y C_ { (/) } ) -> -. -. ( y u. ( { (/) } \ y ) ) = { (/) } )
24		difss 3248	. . . . . . . . . . . . 13 |- ( { (/) } \ y ) C_ { (/) }
25		unss 3296	. . . . . . . . . . . . . 14 |- ( ( y C_ { (/) } /\ ( { (/) } \ y ) C_ { (/) } ) <-> ( y u. ( { (/) } \ y ) ) C_ { (/) } )
26	25	biimpi 119	. . . . . . . . . . . . 13 |- ( ( y C_ { (/) } /\ ( { (/) } \ y ) C_ { (/) } ) -> ( y u. ( { (/) } \ y ) ) C_ { (/) } )
27	24, 26	mpan2 422	. . . . . . . . . . . 12 |- ( y C_ { (/) } -> ( y u. ( { (/) } \ y ) ) C_ { (/) } )
28	27	adantl 275	. . . . . . . . . . 11 |- ( ( ph /\ y C_ { (/) } ) -> ( y u. ( { (/) } \ y ) ) C_ { (/) } )
29		exmid1stab.x	. . . . . . . . . . . . . 14 |- ( ( ph /\ x C_ { (/) } ) -> STAB x = { (/) } )
30	29	ex 114	. . . . . . . . . . . . 13 |- ( ph -> ( x C_ { (/) } -> STAB x = { (/) } ) )
31	30	alrimiv 1862	. . . . . . . . . . . 12 |- ( ph -> A. x ( x C_ { (/) } -> STAB x = { (/) } ) )
32		p0ex 4167	. . . . . . . . . . . . . 14 |- { (/) } e. _V
33	32	ssex 4119	. . . . . . . . . . . . 13 |- ( ( y u. ( { (/) } \ y ) ) C_ { (/) } -> ( y u. ( { (/) } \ y ) ) e. _V )
34		sseq1 3165	. . . . . . . . . . . . . . 15 |- ( x = ( y u. ( { (/) } \ y ) ) -> ( x C_ { (/) } <-> ( y u. ( { (/) } \ y ) ) C_ { (/) } ) )
35		eqeq1 2172	. . . . . . . . . . . . . . . 16 |- ( x = ( y u. ( { (/) } \ y ) ) -> ( x = { (/) } <-> ( y u. ( { (/) } \ y ) ) = { (/) } ) )
36	35	stbid 822	. . . . . . . . . . . . . . 15 |- ( x = ( y u. ( { (/) } \ y ) ) -> (STAB x = { (/) } <-> STAB ( y u. ( { (/) } \ y ) ) = { (/) } ) )
37	34, 36	imbi12d 233	. . . . . . . . . . . . . 14 |- ( x = ( y u. ( { (/) } \ y ) ) -> ( ( x C_ { (/) } -> STAB x = { (/) } ) <-> ( ( y u. ( { (/) } \ y ) ) C_ { (/) } -> STAB ( y u. ( { (/) } \ y ) ) = { (/) } ) ) )
38	37	spcgv 2813	. . . . . . . . . . . . 13 |- ( ( y u. ( { (/) } \ y ) ) e. _V -> ( A. x ( x C_ { (/) } -> STAB x = { (/) } ) -> ( ( y u. ( { (/) } \ y ) ) C_ { (/) } -> STAB ( y u. ( { (/) } \ y ) ) = { (/) } ) ) )
39	27, 33, 38	3syl 17	. . . . . . . . . . . 12 |- ( y C_ { (/) } -> ( A. x ( x C_ { (/) } -> STAB x = { (/) } ) -> ( ( y u. ( { (/) } \ y ) ) C_ { (/) } -> STAB ( y u. ( { (/) } \ y ) ) = { (/) } ) ) )
40	31, 39	mpan9 279	. . . . . . . . . . 11 |- ( ( ph /\ y C_ { (/) } ) -> ( ( y u. ( { (/) } \ y ) ) C_ { (/) } -> STAB ( y u. ( { (/) } \ y ) ) = { (/) } ) )
41	28, 40	mpd 13	. . . . . . . . . 10 |- ( ( ph /\ y C_ { (/) } ) -> STAB ( y u. ( { (/) } \ y ) ) = { (/) } )
42		df-stab 821	. . . . . . . . . 10 |- (STAB ( y u. ( { (/) } \ y ) ) = { (/) } <-> ( -. -. ( y u. ( { (/) } \ y ) ) = { (/) } -> ( y u. ( { (/) } \ y ) ) = { (/) } ) )
43	41, 42	sylib 121	. . . . . . . . 9 |- ( ( ph /\ y C_ { (/) } ) -> ( -. -. ( y u. ( { (/) } \ y ) ) = { (/) } -> ( y u. ( { (/) } \ y ) ) = { (/) } ) )
44	23, 43	mpd 13	. . . . . . . 8 |- ( ( ph /\ y C_ { (/) } ) -> ( y u. ( { (/) } \ y ) ) = { (/) } )
45	2, 44	eleqtrrid 2256	. . . . . . 7 |- ( ( ph /\ y C_ { (/) } ) -> (/) e. ( y u. ( { (/) } \ y ) ) )
46		elun 3263	. . . . . . 7 |- ( (/) e. ( y u. ( { (/) } \ y ) ) <-> ( (/) e. y \/ (/) e. ( { (/) } \ y ) ) )
47	45, 46	sylib 121	. . . . . 6 |- ( ( ph /\ y C_ { (/) } ) -> ( (/) e. y \/ (/) e. ( { (/) } \ y ) ) )
48		eldifn 3245	. . . . . . 7 |- ( (/) e. ( { (/) } \ y ) -> -. (/) e. y )
49	48	orim2i 751	. . . . . 6 |- ( ( (/) e. y \/ (/) e. ( { (/) } \ y ) ) -> ( (/) e. y \/ -. (/) e. y ) )
50	47, 49	syl 14	. . . . 5 |- ( ( ph /\ y C_ { (/) } ) -> ( (/) e. y \/ -. (/) e. y ) )
51		df-dc 825	. . . . 5 |- (DECID (/) e. y <-> ( (/) e. y \/ -. (/) e. y ) )
52	50, 51	sylibr 133	. . . 4 |- ( ( ph /\ y C_ { (/) } ) -> DECID (/) e. y )
53	52	ex 114	. . 3 |- ( ph -> ( y C_ { (/) } -> DECID (/) e. y ) )
54	53	alrimiv 1862	. 2 |- ( ph -> A. y ( y C_ { (/) } -> DECID (/) e. y ) )
55		df-exmid 4174	. 2 |- (EXMID <-> A. y ( y C_ { (/) } -> DECID (/) e. y ) )
56	54, 55	sylibr 133	1 |- ( ph -> EXMID )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 103   \/ wo 698  STAB wstab 820  DECID wdc 824   A.wal 1341   = wceq 1343   e. wcel 2136   =/= wne 2336   _Vcvv 2726   \ cdif 3113   u. cun 3114   C_ wss 3116   (/)c0 3409   {csn 3576  EXMIDwem 4173

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-14 2139  ax-ext 2147  ax-sep 4100  ax-nul 4108  ax-pow 4153

This theorem depends on definitions:  df-bi 116  df-stab 821  df-dc 825  df-tru 1346  df-fal 1349  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2297  df-ne 2337  df-ral 2449  df-rab 2453  df-v 2728  df-dif 3118  df-un 3120  df-in 3122  df-ss 3129  df-nul 3410  df-pw 3561  df-sn 3582  df-exmid 4174

This theorem is referenced by:  subctctexmid  13881