Theorem exmid1stab 4304

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 4221	. . . . . . . . 9 |- (/) e. _V
2	1	snid 3704	. . . . . . . 8 |- (/) e. { (/) }
3		nnexmid 858	. . . . . . . . . . 11 |- -. -. ( y = { (/) } \/ -. y = { (/) } )
4		uneq1 3356	. . . . . . . . . . . . . . 15 |- ( y = { (/) } -> ( y u. ( { (/) } \ y ) ) = ( { (/) } u. ( { (/) } \ y ) ) )
5		undifabs 3573	. . . . . . . . . . . . . . 15 |- ( { (/) } u. ( { (/) } \ y ) ) = { (/) }
6	4, 5	eqtrdi 2280	. . . . . . . . . . . . . 14 |- ( y = { (/) } -> ( y u. ( { (/) } \ y ) ) = { (/) } )
7	6	a1i 9	. . . . . . . . . . . . 13 |- ( y C_ { (/) } -> ( y = { (/) } -> ( y u. ( { (/) } \ y ) ) = { (/) } ) )
8		df-ne 2404	. . . . . . . . . . . . . . . . 17 |- ( y =/= { (/) } <-> -. y = { (/) } )
9		pwntru 4295	. . . . . . . . . . . . . . . . 17 |- ( ( y C_ { (/) } /\ y =/= { (/) } ) -> y = (/) )
10	8, 9	sylan2br 288	. . . . . . . . . . . . . . . 16 |- ( ( y C_ { (/) } /\ -. y = { (/) } ) -> y = (/) )
11	10	difeq2d 3327	. . . . . . . . . . . . . . . . 17 |- ( ( y C_ { (/) } /\ -. y = { (/) } ) -> ( { (/) } \ y ) = ( { (/) } \ (/) ) )
12		dif0 3567	. . . . . . . . . . . . . . . . 17 |- ( { (/) } \ (/) ) = { (/) }
13	11, 12	eqtrdi 2280	. . . . . . . . . . . . . . . 16 |- ( ( y C_ { (/) } /\ -. y = { (/) } ) -> ( { (/) } \ y ) = { (/) } )
14	10, 13	uneq12d 3364	. . . . . . . . . . . . . . 15 |- ( ( y C_ { (/) } /\ -. y = { (/) } ) -> ( y u. ( { (/) } \ y ) ) = ( (/) u. { (/) } ) )
15		uncom 3353	. . . . . . . . . . . . . . . 16 |- ( (/) u. { (/) } ) = ( { (/) } u. (/) )
16		un0 3530	. . . . . . . . . . . . . . . 16 |- ( { (/) } u. (/) ) = { (/) }
17	15, 16	eqtri 2252	. . . . . . . . . . . . . . 15 |- ( (/) u. { (/) } ) = { (/) }
18	14, 17	eqtrdi 2280	. . . . . . . . . . . . . 14 |- ( ( y C_ { (/) } /\ -. y = { (/) } ) -> ( y u. ( { (/) } \ y ) ) = { (/) } )
19	18	ex 115	. . . . . . . . . . . . 13 |- ( y C_ { (/) } -> ( -. y = { (/) } -> ( y u. ( { (/) } \ y ) ) = { (/) } ) )
20	7, 19	jaod 725	. . . . . . . . . . . 12 |- ( y C_ { (/) } -> ( ( y = { (/) } \/ -. y = { (/) } ) -> ( y u. ( { (/) } \ y ) ) = { (/) } ) )
21	20	con3d 636	. . . . . . . . . . 11 |- ( y C_ { (/) } -> ( -. ( y u. ( { (/) } \ y ) ) = { (/) } -> -. ( y = { (/) } \/ -. y = { (/) } ) ) )
22	3, 21	mtoi 670	. . . . . . . . . 10 |- ( y C_ { (/) } -> -. -. ( y u. ( { (/) } \ y ) ) = { (/) } )
23	22	adantl 277	. . . . . . . . 9 |- ( ( ph /\ y C_ { (/) } ) -> -. -. ( y u. ( { (/) } \ y ) ) = { (/) } )
24		difss 3335	. . . . . . . . . . . . 13 |- ( { (/) } \ y ) C_ { (/) }
25		unss 3383	. . . . . . . . . . . . . 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 1922	. . . . . . . . . . . 12 |- ( ph -> A. x ( x C_ { (/) } -> STAB x = { (/) } ) )
32		p0ex 4284	. . . . . . . . . . . . . 14 |- { (/) } e. _V
33	32	ssex 4231	. . . . . . . . . . . . 13 |- ( ( y u. ( { (/) } \ y ) ) C_ { (/) } -> ( y u. ( { (/) } \ y ) ) e. _V )
34		sseq1 3251	. . . . . . . . . . . . . . 15 |- ( x = ( y u. ( { (/) } \ y ) ) -> ( x C_ { (/) } <-> ( y u. ( { (/) } \ y ) ) C_ { (/) } ) )
35		eqeq1 2238	. . . . . . . . . . . . . . . 16 |- ( x = ( y u. ( { (/) } \ y ) ) -> ( x = { (/) } <-> ( y u. ( { (/) } \ y ) ) = { (/) } ) )
36	35	stbid 840	. . . . . . . . . . . . . . 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 2894	. . . . . . . . . . . . 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 839	. . . . . . . . . 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 2321	. . . . . . 7 |- ( ( ph /\ y C_ { (/) } ) -> (/) e. ( y u. ( { (/) } \ y ) ) )
46		elun 3350	. . . . . . 7 |- ( (/) e. ( y u. ( { (/) } \ y ) ) <-> ( (/) e. y \/ (/) e. ( { (/) } \ y ) ) )
47	45, 46	sylib 122	. . . . . 6 |- ( ( ph /\ y C_ { (/) } ) -> ( (/) e. y \/ (/) e. ( { (/) } \ y ) ) )
48		eldifn 3332	. . . . . . 7 |- ( (/) e. ( { (/) } \ y ) -> -. (/) e. y )
49	48	orim2i 769	. . . . . 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 843	. . . . 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 1922	. 2 |- ( ph -> A. y ( y C_ { (/) } -> DECID (/) e. y ) )
55		df-exmid 4291	. 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 716  STAB wstab 838  DECID wdc 842   A.wal 1396   = wceq 1398   e. wcel 2202   =/= wne 2403   _Vcvv 2803   \ cdif 3198   u. cun 3199   C_ wss 3201   (/)c0 3496   {csn 3673  EXMIDwem 4290

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 619  ax-in2 620  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-14 2205  ax-ext 2213  ax-sep 4212  ax-nul 4220  ax-pow 4270

This theorem depends on definitions:  df-bi 117  df-stab 839  df-dc 843  df-tru 1401  df-fal 1404  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-ne 2404  df-ral 2516  df-rab 2520  df-v 2805  df-dif 3203  df-un 3205  df-in 3207  df-ss 3214  df-nul 3497  df-pw 3658  df-sn 3679  df-exmid 4291

This theorem is referenced by:  2omotap  7521  subctctexmid  16705  exmidnotnotr  16710