Theorem undifexmid 4125

Description: Union of complementary parts producing the whole and excluded middle. Although special cases such as undifss 3448 and undifdcss 6819 are provable, the full statement implies excluded middle as shown here. (Contributed by Jim Kingdon, 16-Jun-2022.)

Hypothesis

Ref	Expression
undifexmid.1	|- ( x C_ y <-> ( x u. ( y \ x ) ) = y )

Assertion

Ref	Expression
undifexmid	|- ( ph \/ -. ph )

Distinct variable group:   ph, x, y

Proof of Theorem undifexmid

Dummy variable z is distinct from all other variables.

Step	Hyp	Ref	Expression
1		0ex 4063	. . . . 5 |- (/) e. _V
2	1	snid 3563	. . . 4 |- (/) e. { (/) }
3		ssrab2 3187	. . . . 5 |- { z e. { (/) } | ph } C_ { (/) }
4		p0ex 4120	. . . . . . 7 |- { (/) } e. _V
5	4	rabex 4080	. . . . . 6 |- { z e. { (/) } | ph } e. _V
6		sseq12 3127	. . . . . . 7 |- ( ( x = { z e. { (/) } | ph } /\ y = { (/) } ) -> ( x C_ y <-> { z e. { (/) } | ph } C_ { (/) } ) )
7		simpl 108	. . . . . . . . 9 |- ( ( x = { z e. { (/) } | ph } /\ y = { (/) } ) -> x = { z e. { (/) } | ph } )
8		simpr 109	. . . . . . . . . 10 |- ( ( x = { z e. { (/) } | ph } /\ y = { (/) } ) -> y = { (/) } )
9	8, 7	difeq12d 3200	. . . . . . . . 9 |- ( ( x = { z e. { (/) } | ph } /\ y = { (/) } ) -> ( y \ x ) = ( { (/) } \ { z e. { (/) } | ph } ) )
10	7, 9	uneq12d 3236	. . . . . . . 8 |- ( ( x = { z e. { (/) } | ph } /\ y = { (/) } ) -> ( x u. ( y \ x ) ) = ( { z e. { (/) } | ph } u. ( { (/) } \ { z e. { (/) } | ph } ) ) )
11	10, 8	eqeq12d 2155	. . . . . . 7 |- ( ( x = { z e. { (/) } | ph } /\ y = { (/) } ) -> ( ( x u. ( y \ x ) ) = y <-> ( { z e. { (/) } | ph } u. ( { (/) } \ { z e. { (/) } | ph } ) ) = { (/) } ) )
12	6, 11	bibi12d 234	. . . . . 6 |- ( ( x = { z e. { (/) } | ph } /\ y = { (/) } ) -> ( ( x C_ y <-> ( x u. ( y \ x ) ) = y ) <-> ( { z e. { (/) } | ph } C_ { (/) } <-> ( { z e. { (/) } | ph } u. ( { (/) } \ { z e. { (/) } | ph } ) ) = { (/) } ) ) )
13		undifexmid.1	. . . . . 6 |- ( x C_ y <-> ( x u. ( y \ x ) ) = y )
14	5, 4, 12, 13	vtocl2 2744	. . . . 5 |- ( { z e. { (/) } | ph } C_ { (/) } <-> ( { z e. { (/) } | ph } u. ( { (/) } \ { z e. { (/) } | ph } ) ) = { (/) } )
15	3, 14	mpbi 144	. . . 4 |- ( { z e. { (/) } | ph } u. ( { (/) } \ { z e. { (/) } | ph } ) ) = { (/) }
16	2, 15	eleqtrri 2216	. . 3 |- (/) e. ( { z e. { (/) } | ph } u. ( { (/) } \ { z e. { (/) } | ph } ) )
17		elun 3222	. . 3 |- ( (/) e. ( { z e. { (/) } | ph } u. ( { (/) } \ { z e. { (/) } | ph } ) ) <-> ( (/) e. { z e. { (/) } | ph } \/ (/) e. ( { (/) } \ { z e. { (/) } | ph } ) ) )
18	16, 17	mpbi 144	. 2 |- ( (/) e. { z e. { (/) } | ph } \/ (/) e. ( { (/) } \ { z e. { (/) } | ph } ) )
19		biidd 171	. . . . . 6 |- ( z = (/) -> ( ph <-> ph ) )
20	19	elrab3 2845	. . . . 5 |- ( (/) e. { (/) } -> ( (/) e. { z e. { (/) } | ph } <-> ph ) )
21	2, 20	ax-mp 5	. . . 4 |- ( (/) e. { z e. { (/) } | ph } <-> ph )
22	21	biimpi 119	. . 3 |- ( (/) e. { z e. { (/) } | ph } -> ph )
23		eldifn 3204	. . . 4 |- ( (/) e. ( { (/) } \ { z e. { (/) } | ph } ) -> -. (/) e. { z e. { (/) } | ph } )
24	23, 21	sylnib 666	. . 3 |- ( (/) e. ( { (/) } \ { z e. { (/) } | ph } ) -> -. ph )
25	22, 24	orim12i 749	. 2 |- ( ( (/) e. { z e. { (/) } | ph } \/ (/) e. ( { (/) } \ { z e. { (/) } | ph } ) ) -> ( ph \/ -. ph ) )
26	18, 25	ax-mp 5	1 |- ( ph \/ -. ph )

Syntax hints:   -. wn 3   /\ wa 103   <-> wb 104   \/ wo 698   = wceq 1332   e. wcel 1481   {crab 2421   \ cdif 3073   u. cun 3074   C_ wss 3076   (/)c0 3368   {csn 3532

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 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-14 1493  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-sep 4054  ax-nul 4062  ax-pow 4106

This theorem depends on definitions:  df-bi 116  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ral 2422  df-rab 2426  df-v 2691  df-dif 3078  df-un 3080  df-in 3082  df-ss 3089  df-nul 3369  df-pw 3517  df-sn 3538

This theorem is referenced by: (None)