Theorem undifexmid 4034

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

Hypothesis

Ref	Expression
undifexmid.1	⊢ (𝑥 ⊆ 𝑦 ↔ (𝑥 ∪ (𝑦 ∖ 𝑥)) = 𝑦)

Assertion

Ref	Expression
undifexmid	⊢ (𝜑 ∨ ¬ 𝜑)

Distinct variable group:   𝜑,𝑥,𝑦

Proof of Theorem undifexmid

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		0ex 3972	. . . . 5 ⊢ ∅ ∈ V
2	1	snid 3479	. . . 4 ⊢ ∅ ∈ {∅}
3		ssrab2 3107	. . . . 5 ⊢ {𝑧 ∈ {∅} ∣ 𝜑} ⊆ {∅}
4		p0ex 4029	. . . . . . 7 ⊢ {∅} ∈ V
5	4	rabex 3989	. . . . . 6 ⊢ {𝑧 ∈ {∅} ∣ 𝜑} ∈ V
6		sseq12 3050	. . . . . . 7 ⊢ ((𝑥 = {𝑧 ∈ {∅} ∣ 𝜑} ∧ 𝑦 = {∅}) → (𝑥 ⊆ 𝑦 ↔ {𝑧 ∈ {∅} ∣ 𝜑} ⊆ {∅}))
7		simpl 108	. . . . . . . . 9 ⊢ ((𝑥 = {𝑧 ∈ {∅} ∣ 𝜑} ∧ 𝑦 = {∅}) → 𝑥 = {𝑧 ∈ {∅} ∣ 𝜑})
8		simpr 109	. . . . . . . . . 10 ⊢ ((𝑥 = {𝑧 ∈ {∅} ∣ 𝜑} ∧ 𝑦 = {∅}) → 𝑦 = {∅})
9	8, 7	difeq12d 3120	. . . . . . . . 9 ⊢ ((𝑥 = {𝑧 ∈ {∅} ∣ 𝜑} ∧ 𝑦 = {∅}) → (𝑦 ∖ 𝑥) = ({∅} ∖ {𝑧 ∈ {∅} ∣ 𝜑}))
10	7, 9	uneq12d 3156	. . . . . . . 8 ⊢ ((𝑥 = {𝑧 ∈ {∅} ∣ 𝜑} ∧ 𝑦 = {∅}) → (𝑥 ∪ (𝑦 ∖ 𝑥)) = ({𝑧 ∈ {∅} ∣ 𝜑} ∪ ({∅} ∖ {𝑧 ∈ {∅} ∣ 𝜑})))
11	10, 8	eqeq12d 2103	. . . . . . 7 ⊢ ((𝑥 = {𝑧 ∈ {∅} ∣ 𝜑} ∧ 𝑦 = {∅}) → ((𝑥 ∪ (𝑦 ∖ 𝑥)) = 𝑦 ↔ ({𝑧 ∈ {∅} ∣ 𝜑} ∪ ({∅} ∖ {𝑧 ∈ {∅} ∣ 𝜑})) = {∅}))
12	6, 11	bibi12d 234	. . . . . 6 ⊢ ((𝑥 = {𝑧 ∈ {∅} ∣ 𝜑} ∧ 𝑦 = {∅}) → ((𝑥 ⊆ 𝑦 ↔ (𝑥 ∪ (𝑦 ∖ 𝑥)) = 𝑦) ↔ ({𝑧 ∈ {∅} ∣ 𝜑} ⊆ {∅} ↔ ({𝑧 ∈ {∅} ∣ 𝜑} ∪ ({∅} ∖ {𝑧 ∈ {∅} ∣ 𝜑})) = {∅})))
13		undifexmid.1	. . . . . 6 ⊢ (𝑥 ⊆ 𝑦 ↔ (𝑥 ∪ (𝑦 ∖ 𝑥)) = 𝑦)
14	5, 4, 12, 13	vtocl2 2675	. . . . 5 ⊢ ({𝑧 ∈ {∅} ∣ 𝜑} ⊆ {∅} ↔ ({𝑧 ∈ {∅} ∣ 𝜑} ∪ ({∅} ∖ {𝑧 ∈ {∅} ∣ 𝜑})) = {∅})
15	3, 14	mpbi 144	. . . 4 ⊢ ({𝑧 ∈ {∅} ∣ 𝜑} ∪ ({∅} ∖ {𝑧 ∈ {∅} ∣ 𝜑})) = {∅}
16	2, 15	eleqtrri 2164	. . 3 ⊢ ∅ ∈ ({𝑧 ∈ {∅} ∣ 𝜑} ∪ ({∅} ∖ {𝑧 ∈ {∅} ∣ 𝜑}))
17		elun 3142	. . 3 ⊢ (∅ ∈ ({𝑧 ∈ {∅} ∣ 𝜑} ∪ ({∅} ∖ {𝑧 ∈ {∅} ∣ 𝜑})) ↔ (∅ ∈ {𝑧 ∈ {∅} ∣ 𝜑} ∨ ∅ ∈ ({∅} ∖ {𝑧 ∈ {∅} ∣ 𝜑})))
18	16, 17	mpbi 144	. 2 ⊢ (∅ ∈ {𝑧 ∈ {∅} ∣ 𝜑} ∨ ∅ ∈ ({∅} ∖ {𝑧 ∈ {∅} ∣ 𝜑}))
19		biidd 171	. . . . . 6 ⊢ (𝑧 = ∅ → (𝜑 ↔ 𝜑))
20	19	elrab3 2773	. . . . 5 ⊢ (∅ ∈ {∅} → (∅ ∈ {𝑧 ∈ {∅} ∣ 𝜑} ↔ 𝜑))
21	2, 20	ax-mp 7	. . . 4 ⊢ (∅ ∈ {𝑧 ∈ {∅} ∣ 𝜑} ↔ 𝜑)
22	21	biimpi 119	. . 3 ⊢ (∅ ∈ {𝑧 ∈ {∅} ∣ 𝜑} → 𝜑)
23		eldifn 3124	. . . 4 ⊢ (∅ ∈ ({∅} ∖ {𝑧 ∈ {∅} ∣ 𝜑}) → ¬ ∅ ∈ {𝑧 ∈ {∅} ∣ 𝜑})
24	23, 21	sylnib 637	. . 3 ⊢ (∅ ∈ ({∅} ∖ {𝑧 ∈ {∅} ∣ 𝜑}) → ¬ 𝜑)
25	22, 24	orim12i 712	. 2 ⊢ ((∅ ∈ {𝑧 ∈ {∅} ∣ 𝜑} ∨ ∅ ∈ ({∅} ∖ {𝑧 ∈ {∅} ∣ 𝜑})) → (𝜑 ∨ ¬ 𝜑))
26	18, 25	ax-mp 7	1 ⊢ (𝜑 ∨ ¬ 𝜑)

Syntax hints:  ¬ wn 3   ∧ wa 103   ↔ wb 104   ∨ wo 665   = wceq 1290   ∈ wcel 1439  {crab 2364   ∖ cdif 2997   ∪ cun 2998   ⊆ wss 3000  ∅c0 3287  {csn 3450

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 580  ax-in2 581  ax-io 666  ax-5 1382  ax-7 1383  ax-gen 1384  ax-ie1 1428  ax-ie2 1429  ax-8 1441  ax-10 1442  ax-11 1443  ax-i12 1444  ax-bndl 1445  ax-4 1446  ax-14 1451  ax-17 1465  ax-i9 1469  ax-ial 1473  ax-i5r 1474  ax-ext 2071  ax-sep 3963  ax-nul 3971  ax-pow 4015

This theorem depends on definitions:  df-bi 116  df-tru 1293  df-nf 1396  df-sb 1694  df-clab 2076  df-cleq 2082  df-clel 2085  df-nfc 2218  df-ral 2365  df-rab 2369  df-v 2622  df-dif 3002  df-un 3004  df-in 3006  df-ss 3013  df-nul 3288  df-pw 3435  df-sn 3456

This theorem is referenced by: (None)