Theorem exmid1stab 4251

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 4170	. . . . . . . . 9 |- (/) e. _V
2	1	snid 3663	. . . . . . . 8 |- (/) e. { (/) }
3		nnexmid 851	. . . . . . . . . . 11 |- -. -. ( y = { (/) } \/ -. y = { (/) } )
4		uneq1 3319	. . . . . . . . . . . . . . 15 |- ( y = { (/) } -> ( y u. ( { (/) } \ y ) ) = ( { (/) } u. ( { (/) } \ y ) ) )
5		undifabs 3536	. . . . . . . . . . . . . . 15 |- ( { (/) } u. ( { (/) } \ y ) ) = { (/) }
6	4, 5	eqtrdi 2253	. . . . . . . . . . . . . 14 |- ( y = { (/) } -> ( y u. ( { (/) } \ y ) ) = { (/) } )
7	6	a1i 9	. . . . . . . . . . . . 13 |- ( y C_ { (/) } -> ( y = { (/) } -> ( y u. ( { (/) } \ y ) ) = { (/) } ) )
8		df-ne 2376	. . . . . . . . . . . . . . . . 17 |- ( y =/= { (/) } <-> -. y = { (/) } )
9		pwntru 4242	. . . . . . . . . . . . . . . . 17 |- ( ( y C_ { (/) } /\ y =/= { (/) } ) -> y = (/) )
10	8, 9	sylan2br 288	. . . . . . . . . . . . . . . 16 |- ( ( y C_ { (/) } /\ -. y = { (/) } ) -> y = (/) )
11	10	difeq2d 3290	. . . . . . . . . . . . . . . . 17 |- ( ( y C_ { (/) } /\ -. y = { (/) } ) -> ( { (/) } \ y ) = ( { (/) } \ (/) ) )
12		dif0 3530	. . . . . . . . . . . . . . . . 17 |- ( { (/) } \ (/) ) = { (/) }
13	11, 12	eqtrdi 2253	. . . . . . . . . . . . . . . 16 |- ( ( y C_ { (/) } /\ -. y = { (/) } ) -> ( { (/) } \ y ) = { (/) } )
14	10, 13	uneq12d 3327	. . . . . . . . . . . . . . 15 |- ( ( y C_ { (/) } /\ -. y = { (/) } ) -> ( y u. ( { (/) } \ y ) ) = ( (/) u. { (/) } ) )
15		uncom 3316	. . . . . . . . . . . . . . . 16 |- ( (/) u. { (/) } ) = ( { (/) } u. (/) )
16		un0 3493	. . . . . . . . . . . . . . . 16 |- ( { (/) } u. (/) ) = { (/) }
17	15, 16	eqtri 2225	. . . . . . . . . . . . . . 15 |- ( (/) u. { (/) } ) = { (/) }
18	14, 17	eqtrdi 2253	. . . . . . . . . . . . . 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 3298	. . . . . . . . . . . . 13 |- ( { (/) } \ y ) C_ { (/) }
25		unss 3346	. . . . . . . . . . . . . 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 1896	. . . . . . . . . . . 12 |- ( ph -> A. x ( x C_ { (/) } -> STAB x = { (/) } ) )
32		p0ex 4231	. . . . . . . . . . . . . 14 |- { (/) } e. _V
33	32	ssex 4180	. . . . . . . . . . . . 13 |- ( ( y u. ( { (/) } \ y ) ) C_ { (/) } -> ( y u. ( { (/) } \ y ) ) e. _V )
34		sseq1 3215	. . . . . . . . . . . . . . 15 |- ( x = ( y u. ( { (/) } \ y ) ) -> ( x C_ { (/) } <-> ( y u. ( { (/) } \ y ) ) C_ { (/) } ) )
35		eqeq1 2211	. . . . . . . . . . . . . . . 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 2859	. . . . . . . . . . . . 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 2294	. . . . . . 7 |- ( ( ph /\ y C_ { (/) } ) -> (/) e. ( y u. ( { (/) } \ y ) ) )
46		elun 3313	. . . . . . 7 |- ( (/) e. ( y u. ( { (/) } \ y ) ) <-> ( (/) e. y \/ (/) e. ( { (/) } \ y ) ) )
47	45, 46	sylib 122	. . . . . 6 |- ( ( ph /\ y C_ { (/) } ) -> ( (/) e. y \/ (/) e. ( { (/) } \ y ) ) )
48		eldifn 3295	. . . . . . 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 1896	. 2 |- ( ph -> A. y ( y C_ { (/) } -> DECID (/) e. y ) )
55		df-exmid 4238	. 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 1370   = wceq 1372   e. wcel 2175   =/= wne 2375   _Vcvv 2771   \ cdif 3162   u. cun 3163   C_ wss 3165   (/)c0 3459   {csn 3632  EXMIDwem 4237

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 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-14 2178  ax-ext 2186  ax-sep 4161  ax-nul 4169  ax-pow 4217

This theorem depends on definitions:  df-bi 117  df-stab 832  df-dc 836  df-tru 1375  df-fal 1378  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-ne 2376  df-ral 2488  df-rab 2492  df-v 2773  df-dif 3167  df-un 3169  df-in 3171  df-ss 3178  df-nul 3460  df-pw 3617  df-sn 3638  df-exmid 4238

This theorem is referenced by:  2omotap  7370  subctctexmid  15899