Theorem exmid1stab 4209

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 4131	. . . . . . . . 9 |- (/) e. _V
2	1	snid 3624	. . . . . . . 8 |- (/) e. { (/) }
3		nnexmid 850	. . . . . . . . . . 11 |- -. -. ( y = { (/) } \/ -. y = { (/) } )
4		uneq1 3283	. . . . . . . . . . . . . . 15 |- ( y = { (/) } -> ( y u. ( { (/) } \ y ) ) = ( { (/) } u. ( { (/) } \ y ) ) )
5		undifabs 3500	. . . . . . . . . . . . . . 15 |- ( { (/) } u. ( { (/) } \ y ) ) = { (/) }
6	4, 5	eqtrdi 2226	. . . . . . . . . . . . . 14 |- ( y = { (/) } -> ( y u. ( { (/) } \ y ) ) = { (/) } )
7	6	a1i 9	. . . . . . . . . . . . 13 |- ( y C_ { (/) } -> ( y = { (/) } -> ( y u. ( { (/) } \ y ) ) = { (/) } ) )
8		df-ne 2348	. . . . . . . . . . . . . . . . 17 |- ( y =/= { (/) } <-> -. y = { (/) } )
9		pwntru 4200	. . . . . . . . . . . . . . . . 17 |- ( ( y C_ { (/) } /\ y =/= { (/) } ) -> y = (/) )
10	8, 9	sylan2br 288	. . . . . . . . . . . . . . . 16 |- ( ( y C_ { (/) } /\ -. y = { (/) } ) -> y = (/) )
11	10	difeq2d 3254	. . . . . . . . . . . . . . . . 17 |- ( ( y C_ { (/) } /\ -. y = { (/) } ) -> ( { (/) } \ y ) = ( { (/) } \ (/) ) )
12		dif0 3494	. . . . . . . . . . . . . . . . 17 |- ( { (/) } \ (/) ) = { (/) }
13	11, 12	eqtrdi 2226	. . . . . . . . . . . . . . . 16 |- ( ( y C_ { (/) } /\ -. y = { (/) } ) -> ( { (/) } \ y ) = { (/) } )
14	10, 13	uneq12d 3291	. . . . . . . . . . . . . . 15 |- ( ( y C_ { (/) } /\ -. y = { (/) } ) -> ( y u. ( { (/) } \ y ) ) = ( (/) u. { (/) } ) )
15		uncom 3280	. . . . . . . . . . . . . . . 16 |- ( (/) u. { (/) } ) = ( { (/) } u. (/) )
16		un0 3457	. . . . . . . . . . . . . . . 16 |- ( { (/) } u. (/) ) = { (/) }
17	15, 16	eqtri 2198	. . . . . . . . . . . . . . 15 |- ( (/) u. { (/) } ) = { (/) }
18	14, 17	eqtrdi 2226	. . . . . . . . . . . . . 14 |- ( ( y C_ { (/) } /\ -. y = { (/) } ) -> ( y u. ( { (/) } \ y ) ) = { (/) } )
19	18	ex 115	. . . . . . . . . . . . 13 |- ( y C_ { (/) } -> ( -. y = { (/) } -> ( y u. ( { (/) } \ y ) ) = { (/) } ) )
20	7, 19	jaod 717	. . . . . . . . . . . 12 |- ( y C_ { (/) } -> ( ( y = { (/) } \/ -. y = { (/) } ) -> ( y u. ( { (/) } \ y ) ) = { (/) } ) )
21	20	con3d 631	. . . . . . . . . . 11 |- ( y C_ { (/) } -> ( -. ( y u. ( { (/) } \ y ) ) = { (/) } -> -. ( y = { (/) } \/ -. y = { (/) } ) ) )
22	3, 21	mtoi 664	. . . . . . . . . 10 |- ( y C_ { (/) } -> -. -. ( y u. ( { (/) } \ y ) ) = { (/) } )
23	22	adantl 277	. . . . . . . . 9 |- ( ( ph /\ y C_ { (/) } ) -> -. -. ( y u. ( { (/) } \ y ) ) = { (/) } )
24		difss 3262	. . . . . . . . . . . . 13 |- ( { (/) } \ y ) C_ { (/) }
25		unss 3310	. . . . . . . . . . . . . 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 1874	. . . . . . . . . . . 12 |- ( ph -> A. x ( x C_ { (/) } -> STAB x = { (/) } ) )
32		p0ex 4189	. . . . . . . . . . . . . 14 |- { (/) } e. _V
33	32	ssex 4141	. . . . . . . . . . . . 13 |- ( ( y u. ( { (/) } \ y ) ) C_ { (/) } -> ( y u. ( { (/) } \ y ) ) e. _V )
34		sseq1 3179	. . . . . . . . . . . . . . 15 |- ( x = ( y u. ( { (/) } \ y ) ) -> ( x C_ { (/) } <-> ( y u. ( { (/) } \ y ) ) C_ { (/) } ) )
35		eqeq1 2184	. . . . . . . . . . . . . . . 16 |- ( x = ( y u. ( { (/) } \ y ) ) -> ( x = { (/) } <-> ( y u. ( { (/) } \ y ) ) = { (/) } ) )
36	35	stbid 832	. . . . . . . . . . . . . . 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 2825	. . . . . . . . . . . . 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 831	. . . . . . . . . 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 2267	. . . . . . 7 |- ( ( ph /\ y C_ { (/) } ) -> (/) e. ( y u. ( { (/) } \ y ) ) )
46		elun 3277	. . . . . . 7 |- ( (/) e. ( y u. ( { (/) } \ y ) ) <-> ( (/) e. y \/ (/) e. ( { (/) } \ y ) ) )
47	45, 46	sylib 122	. . . . . 6 |- ( ( ph /\ y C_ { (/) } ) -> ( (/) e. y \/ (/) e. ( { (/) } \ y ) ) )
48		eldifn 3259	. . . . . . 7 |- ( (/) e. ( { (/) } \ y ) -> -. (/) e. y )
49	48	orim2i 761	. . . . . 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 835	. . . . 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 1874	. 2 |- ( ph -> A. y ( y C_ { (/) } -> DECID (/) e. y ) )
55		df-exmid 4196	. 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 708  STAB wstab 830  DECID wdc 834   A.wal 1351   = wceq 1353   e. wcel 2148   =/= wne 2347   _Vcvv 2738   \ cdif 3127   u. cun 3128   C_ wss 3130   (/)c0 3423   {csn 3593  EXMIDwem 4195

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 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-14 2151  ax-ext 2159  ax-sep 4122  ax-nul 4130  ax-pow 4175

This theorem depends on definitions:  df-bi 117  df-stab 831  df-dc 835  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-ral 2460  df-rab 2464  df-v 2740  df-dif 3132  df-un 3134  df-in 3136  df-ss 3143  df-nul 3424  df-pw 3578  df-sn 3599  df-exmid 4196

This theorem is referenced by:  2omotap  7258  subctctexmid  14753