Theorem exmid1stab 4220

Description: If every 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 4142	. . . . . . . . 9 |- (/) e. _V
2	1	snid 3635	. . . . . . . 8 |- (/) e. { (/) }
3		nnexmid 851	. . . . . . . . . . 11 |- -. -. ( y = { (/) } \/ -. y = { (/) } )
4		uneq1 3294	. . . . . . . . . . . . . . 15 |- ( y = { (/) } -> ( y u. ( { (/) } \ y ) ) = ( { (/) } u. ( { (/) } \ y ) ) )
5		undifabs 3511	. . . . . . . . . . . . . . 15 |- ( { (/) } u. ( { (/) } \ y ) ) = { (/) }
6	4, 5	eqtrdi 2236	. . . . . . . . . . . . . 14 |- ( y = { (/) } -> ( y u. ( { (/) } \ y ) ) = { (/) } )
7	6	a1i 9	. . . . . . . . . . . . 13 |- ( y C_ { (/) } -> ( y = { (/) } -> ( y u. ( { (/) } \ y ) ) = { (/) } ) )
8		df-ne 2358	. . . . . . . . . . . . . . . . 17 |- ( y =/= { (/) } <-> -. y = { (/) } )
9		pwntru 4211	. . . . . . . . . . . . . . . . 17 |- ( ( y C_ { (/) } /\ y =/= { (/) } ) -> y = (/) )
10	8, 9	sylan2br 288	. . . . . . . . . . . . . . . 16 |- ( ( y C_ { (/) } /\ -. y = { (/) } ) -> y = (/) )
11	10	difeq2d 3265	. . . . . . . . . . . . . . . . 17 |- ( ( y C_ { (/) } /\ -. y = { (/) } ) -> ( { (/) } \ y ) = ( { (/) } \ (/) ) )
12		dif0 3505	. . . . . . . . . . . . . . . . 17 |- ( { (/) } \ (/) ) = { (/) }
13	11, 12	eqtrdi 2236	. . . . . . . . . . . . . . . 16 |- ( ( y C_ { (/) } /\ -. y = { (/) } ) -> ( { (/) } \ y ) = { (/) } )
14	10, 13	uneq12d 3302	. . . . . . . . . . . . . . 15 |- ( ( y C_ { (/) } /\ -. y = { (/) } ) -> ( y u. ( { (/) } \ y ) ) = ( (/) u. { (/) } ) )
15		uncom 3291	. . . . . . . . . . . . . . . 16 |- ( (/) u. { (/) } ) = ( { (/) } u. (/) )
16		un0 3468	. . . . . . . . . . . . . . . 16 |- ( { (/) } u. (/) ) = { (/) }
17	15, 16	eqtri 2208	. . . . . . . . . . . . . . 15 |- ( (/) u. { (/) } ) = { (/) }
18	14, 17	eqtrdi 2236	. . . . . . . . . . . . . 14 |- ( ( y C_ { (/) } /\ -. y = { (/) } ) -> ( y u. ( { (/) } \ y ) ) = { (/) } )
19	18	ex 115	. . . . . . . . . . . . 13 |- ( y C_ { (/) } -> ( -. y = { (/) } -> ( y u. ( { (/) } \ y ) ) = { (/) } ) )
20	7, 19	jaod 718	. . . . . . . . . . . 12 |- ( y C_ { (/) } -> ( ( y = { (/) } \/ -. y = { (/) } ) -> ( y u. ( { (/) } \ y ) ) = { (/) } ) )
21	20	con3d 632	. . . . . . . . . . 11 |- ( y C_ { (/) } -> ( -. ( y u. ( { (/) } \ y ) ) = { (/) } -> -. ( y = { (/) } \/ -. y = { (/) } ) ) )
22	3, 21	mtoi 665	. . . . . . . . . 10 |- ( y C_ { (/) } -> -. -. ( y u. ( { (/) } \ y ) ) = { (/) } )
23	22	adantl 277	. . . . . . . . 9 |- ( ( ph /\ y C_ { (/) } ) -> -. -. ( y u. ( { (/) } \ y ) ) = { (/) } )
24		difss 3273	. . . . . . . . . . . . 13 |- ( { (/) } \ y ) C_ { (/) }
25		unss 3321	. . . . . . . . . . . . . 14 |- ( ( y C_ { (/) } /\ ( { (/) } \ y ) C_ { (/) } ) <-> ( y u. ( { (/) } \ y ) ) C_ { (/) } )
26	25	biimpi 120	. . . . . . . . . . . . 13 |- ( ( y C_ { (/) } /\ ( { (/) } \ y ) C_ { (/) } ) -> ( y u. ( { (/) } \ y ) ) C_ { (/) } )
27	24, 26	mpan2 425	. . . . . . . . . . . 12 |- ( y C_ { (/) } -> ( y u. ( { (/) } \ y ) ) C_ { (/) } )
28	27	adantl 277	. . . . . . . . . . 11 |- ( ( ph /\ y C_ { (/) } ) -> ( y u. ( { (/) } \ y ) ) C_ { (/) } )
29		exmid1stab.x	. . . . . . . . . . . . . 14 |- ( ( ph /\ x C_ { (/) } ) -> STAB x = { (/) } )
30	29	ex 115	. . . . . . . . . . . . 13 |- ( ph -> ( x C_ { (/) } -> STAB x = { (/) } ) )
31	30	alrimiv 1884	. . . . . . . . . . . 12 |- ( ph -> A. x ( x C_ { (/) } -> STAB x = { (/) } ) )
32		p0ex 4200	. . . . . . . . . . . . . 14 |- { (/) } e. _V
33	32	ssex 4152	. . . . . . . . . . . . 13 |- ( ( y u. ( { (/) } \ y ) ) C_ { (/) } -> ( y u. ( { (/) } \ y ) ) e. _V )
34		sseq1 3190	. . . . . . . . . . . . . . 15 |- ( x = ( y u. ( { (/) } \ y ) ) -> ( x C_ { (/) } <-> ( y u. ( { (/) } \ y ) ) C_ { (/) } ) )
35		eqeq1 2194	. . . . . . . . . . . . . . . 16 |- ( x = ( y u. ( { (/) } \ y ) ) -> ( x = { (/) } <-> ( y u. ( { (/) } \ y ) ) = { (/) } ) )
36	35	stbid 833	. . . . . . . . . . . . . . 15 |- ( x = ( y u. ( { (/) } \ y ) ) -> (STAB x = { (/) } <-> STAB ( y u. ( { (/) } \ y ) ) = { (/) } ) )
37	34, 36	imbi12d 234	. . . . . . . . . . . . . 14 |- ( x = ( y u. ( { (/) } \ y ) ) -> ( ( x C_ { (/) } -> STAB x = { (/) } ) <-> ( ( y u. ( { (/) } \ y ) ) C_ { (/) } -> STAB ( y u. ( { (/) } \ y ) ) = { (/) } ) ) )
38	37	spcgv 2836	. . . . . . . . . . . . 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 281	. . . . . . . . . . 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 832	. . . . . . . . . 10 |- (STAB ( y u. ( { (/) } \ y ) ) = { (/) } <-> ( -. -. ( y u. ( { (/) } \ y ) ) = { (/) } -> ( y u. ( { (/) } \ y ) ) = { (/) } ) )
43	41, 42	sylib 122	. . . . . . . . 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 2277	. . . . . . 7 |- ( ( ph /\ y C_ { (/) } ) -> (/) e. ( y u. ( { (/) } \ y ) ) )
46		elun 3288	. . . . . . 7 |- ( (/) e. ( y u. ( { (/) } \ y ) ) <-> ( (/) e. y \/ (/) e. ( { (/) } \ y ) ) )
47	45, 46	sylib 122	. . . . . 6 |- ( ( ph /\ y C_ { (/) } ) -> ( (/) e. y \/ (/) e. ( { (/) } \ y ) ) )
48		eldifn 3270	. . . . . . 7 |- ( (/) e. ( { (/) } \ y ) -> -. (/) e. y )
49	48	orim2i 762	. . . . . 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 836	. . . . 5 |- (DECID (/) e. y <-> ( (/) e. y \/ -. (/) e. y ) )
52	50, 51	sylibr 134	. . . 4 |- ( ( ph /\ y C_ { (/) } ) -> DECID (/) e. y )
53	52	ex 115	. . 3 |- ( ph -> ( y C_ { (/) } -> DECID (/) e. y ) )
54	53	alrimiv 1884	. 2 |- ( ph -> A. y ( y C_ { (/) } -> DECID (/) e. y ) )
55		df-exmid 4207	. 2 |- (EXMID <-> A. y ( y C_ { (/) } -> DECID (/) e. y ) )
56	54, 55	sylibr 134	1 |- ( ph -> EXMID )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 104   \/ wo 709  STAB wstab 831  DECID wdc 835   A.wal 1361   = wceq 1363   e. wcel 2158   =/= wne 2357   _Vcvv 2749   \ cdif 3138   u. cun 3139   C_ wss 3141   (/)c0 3434   {csn 3604  EXMIDwem 4206

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 615  ax-in2 616  ax-io 710  ax-5 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-10 1515  ax-11 1516  ax-i12 1517  ax-bndl 1519  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-14 2161  ax-ext 2169  ax-sep 4133  ax-nul 4141  ax-pow 4186

This theorem depends on definitions:  df-bi 117  df-stab 832  df-dc 836  df-tru 1366  df-fal 1369  df-nf 1471  df-sb 1773  df-clab 2174  df-cleq 2180  df-clel 2183  df-nfc 2318  df-ne 2358  df-ral 2470  df-rab 2474  df-v 2751  df-dif 3143  df-un 3145  df-in 3147  df-ss 3154  df-nul 3435  df-pw 3589  df-sn 3610  df-exmid 4207

This theorem is referenced by:  2omotap  7272  subctctexmid  15104