Theorem exmidundif 4203

Description: Excluded middle is equivalent to every subset having a complement. That is, the union of a subset and its relative complement being the whole set. Although special cases such as undifss 3503 and undifdcss 6916 are provable, the full statement is equivalent to excluded middle as shown here. (Contributed by Jim Kingdon, 18-Jun-2022.)

Assertion

Ref	Expression
exmidundif	⊢ (EXMID ↔ ∀𝑥∀𝑦(𝑥 ⊆ 𝑦 ↔ (𝑥 ∪ (𝑦 ∖ 𝑥)) = 𝑦))

Distinct variable group:   𝑥,𝑦

Proof of Theorem exmidundif

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		undifss 3503	. . . . . . . 8 ⊢ (𝑥 ⊆ 𝑦 ↔ (𝑥 ∪ (𝑦 ∖ 𝑥)) ⊆ 𝑦)
2	1	biimpi 120	. . . . . . 7 ⊢ (𝑥 ⊆ 𝑦 → (𝑥 ∪ (𝑦 ∖ 𝑥)) ⊆ 𝑦)
3	2	adantl 277	. . . . . 6 ⊢ ((EXMID ∧ 𝑥 ⊆ 𝑦) → (𝑥 ∪ (𝑦 ∖ 𝑥)) ⊆ 𝑦)
4		elun1 3302	. . . . . . . . . . 11 ⊢ (𝑧 ∈ 𝑥 → 𝑧 ∈ (𝑥 ∪ (𝑦 ∖ 𝑥)))
5	4	adantl 277	. . . . . . . . . 10 ⊢ (((EXMID ∧ 𝑧 ∈ 𝑦) ∧ 𝑧 ∈ 𝑥) → 𝑧 ∈ (𝑥 ∪ (𝑦 ∖ 𝑥)))
6		simplr 528	. . . . . . . . . . . 12 ⊢ (((EXMID ∧ 𝑧 ∈ 𝑦) ∧ ¬ 𝑧 ∈ 𝑥) → 𝑧 ∈ 𝑦)
7		simpr 110	. . . . . . . . . . . 12 ⊢ (((EXMID ∧ 𝑧 ∈ 𝑦) ∧ ¬ 𝑧 ∈ 𝑥) → ¬ 𝑧 ∈ 𝑥)
8	6, 7	eldifd 3139	. . . . . . . . . . 11 ⊢ (((EXMID ∧ 𝑧 ∈ 𝑦) ∧ ¬ 𝑧 ∈ 𝑥) → 𝑧 ∈ (𝑦 ∖ 𝑥))
9		elun2 3303	. . . . . . . . . . 11 ⊢ (𝑧 ∈ (𝑦 ∖ 𝑥) → 𝑧 ∈ (𝑥 ∪ (𝑦 ∖ 𝑥)))
10	8, 9	syl 14	. . . . . . . . . 10 ⊢ (((EXMID ∧ 𝑧 ∈ 𝑦) ∧ ¬ 𝑧 ∈ 𝑥) → 𝑧 ∈ (𝑥 ∪ (𝑦 ∖ 𝑥)))
11		exmidexmid 4193	. . . . . . . . . . . 12 ⊢ (EXMID → DECID 𝑧 ∈ 𝑥)
12		exmiddc 836	. . . . . . . . . . . 12 ⊢ (DECID 𝑧 ∈ 𝑥 → (𝑧 ∈ 𝑥 ∨ ¬ 𝑧 ∈ 𝑥))
13	11, 12	syl 14	. . . . . . . . . . 11 ⊢ (EXMID → (𝑧 ∈ 𝑥 ∨ ¬ 𝑧 ∈ 𝑥))
14	13	adantr 276	. . . . . . . . . 10 ⊢ ((EXMID ∧ 𝑧 ∈ 𝑦) → (𝑧 ∈ 𝑥 ∨ ¬ 𝑧 ∈ 𝑥))
15	5, 10, 14	mpjaodan 798	. . . . . . . . 9 ⊢ ((EXMID ∧ 𝑧 ∈ 𝑦) → 𝑧 ∈ (𝑥 ∪ (𝑦 ∖ 𝑥)))
16	15	ex 115	. . . . . . . 8 ⊢ (EXMID → (𝑧 ∈ 𝑦 → 𝑧 ∈ (𝑥 ∪ (𝑦 ∖ 𝑥))))
17	16	ssrdv 3161	. . . . . . 7 ⊢ (EXMID → 𝑦 ⊆ (𝑥 ∪ (𝑦 ∖ 𝑥)))
18	17	adantr 276	. . . . . 6 ⊢ ((EXMID ∧ 𝑥 ⊆ 𝑦) → 𝑦 ⊆ (𝑥 ∪ (𝑦 ∖ 𝑥)))
19	3, 18	eqssd 3172	. . . . 5 ⊢ ((EXMID ∧ 𝑥 ⊆ 𝑦) → (𝑥 ∪ (𝑦 ∖ 𝑥)) = 𝑦)
20	19	ex 115	. . . 4 ⊢ (EXMID → (𝑥 ⊆ 𝑦 → (𝑥 ∪ (𝑦 ∖ 𝑥)) = 𝑦))
21		ssun1 3298	. . . . 5 ⊢ 𝑥 ⊆ (𝑥 ∪ (𝑦 ∖ 𝑥))
22		sseq2 3179	. . . . 5 ⊢ ((𝑥 ∪ (𝑦 ∖ 𝑥)) = 𝑦 → (𝑥 ⊆ (𝑥 ∪ (𝑦 ∖ 𝑥)) ↔ 𝑥 ⊆ 𝑦))
23	21, 22	mpbii 148	. . . 4 ⊢ ((𝑥 ∪ (𝑦 ∖ 𝑥)) = 𝑦 → 𝑥 ⊆ 𝑦)
24	20, 23	impbid1 142	. . 3 ⊢ (EXMID → (𝑥 ⊆ 𝑦 ↔ (𝑥 ∪ (𝑦 ∖ 𝑥)) = 𝑦))
25	24	alrimivv 1875	. 2 ⊢ (EXMID → ∀𝑥∀𝑦(𝑥 ⊆ 𝑦 ↔ (𝑥 ∪ (𝑦 ∖ 𝑥)) = 𝑦))
26		vex 2740	. . . . . 6 ⊢ 𝑧 ∈ V
27		p0ex 4185	. . . . . 6 ⊢ {∅} ∈ V
28		sseq12 3180	. . . . . . . 8 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = {∅}) → (𝑥 ⊆ 𝑦 ↔ 𝑧 ⊆ {∅}))
29		simpl 109	. . . . . . . . . 10 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = {∅}) → 𝑥 = 𝑧)
30		simpr 110	. . . . . . . . . . 11 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = {∅}) → 𝑦 = {∅})
31	30, 29	difeq12d 3254	. . . . . . . . . 10 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = {∅}) → (𝑦 ∖ 𝑥) = ({∅} ∖ 𝑧))
32	29, 31	uneq12d 3290	. . . . . . . . 9 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = {∅}) → (𝑥 ∪ (𝑦 ∖ 𝑥)) = (𝑧 ∪ ({∅} ∖ 𝑧)))
33	32, 30	eqeq12d 2192	. . . . . . . 8 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = {∅}) → ((𝑥 ∪ (𝑦 ∖ 𝑥)) = 𝑦 ↔ (𝑧 ∪ ({∅} ∖ 𝑧)) = {∅}))
34	28, 33	bibi12d 235	. . . . . . 7 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = {∅}) → ((𝑥 ⊆ 𝑦 ↔ (𝑥 ∪ (𝑦 ∖ 𝑥)) = 𝑦) ↔ (𝑧 ⊆ {∅} ↔ (𝑧 ∪ ({∅} ∖ 𝑧)) = {∅})))
35	34	spc2gv 2828	. . . . . 6 ⊢ ((𝑧 ∈ V ∧ {∅} ∈ V) → (∀𝑥∀𝑦(𝑥 ⊆ 𝑦 ↔ (𝑥 ∪ (𝑦 ∖ 𝑥)) = 𝑦) → (𝑧 ⊆ {∅} ↔ (𝑧 ∪ ({∅} ∖ 𝑧)) = {∅})))
36	26, 27, 35	mp2an 426	. . . . 5 ⊢ (∀𝑥∀𝑦(𝑥 ⊆ 𝑦 ↔ (𝑥 ∪ (𝑦 ∖ 𝑥)) = 𝑦) → (𝑧 ⊆ {∅} ↔ (𝑧 ∪ ({∅} ∖ 𝑧)) = {∅}))
37		0ex 4127	. . . . . . . 8 ⊢ ∅ ∈ V
38	37	snid 3622	. . . . . . 7 ⊢ ∅ ∈ {∅}
39		eleq2 2241	. . . . . . 7 ⊢ ((𝑧 ∪ ({∅} ∖ 𝑧)) = {∅} → (∅ ∈ (𝑧 ∪ ({∅} ∖ 𝑧)) ↔ ∅ ∈ {∅}))
40	38, 39	mpbiri 168	. . . . . 6 ⊢ ((𝑧 ∪ ({∅} ∖ 𝑧)) = {∅} → ∅ ∈ (𝑧 ∪ ({∅} ∖ 𝑧)))
41		eldifn 3258	. . . . . . . 8 ⊢ (∅ ∈ ({∅} ∖ 𝑧) → ¬ ∅ ∈ 𝑧)
42	41	orim2i 761	. . . . . . 7 ⊢ ((∅ ∈ 𝑧 ∨ ∅ ∈ ({∅} ∖ 𝑧)) → (∅ ∈ 𝑧 ∨ ¬ ∅ ∈ 𝑧))
43		elun 3276	. . . . . . 7 ⊢ (∅ ∈ (𝑧 ∪ ({∅} ∖ 𝑧)) ↔ (∅ ∈ 𝑧 ∨ ∅ ∈ ({∅} ∖ 𝑧)))
44		df-dc 835	. . . . . . 7 ⊢ (DECID ∅ ∈ 𝑧 ↔ (∅ ∈ 𝑧 ∨ ¬ ∅ ∈ 𝑧))
45	42, 43, 44	3imtr4i 201	. . . . . 6 ⊢ (∅ ∈ (𝑧 ∪ ({∅} ∖ 𝑧)) → DECID ∅ ∈ 𝑧)
46	40, 45	syl 14	. . . . 5 ⊢ ((𝑧 ∪ ({∅} ∖ 𝑧)) = {∅} → DECID ∅ ∈ 𝑧)
47	36, 46	syl6bi 163	. . . 4 ⊢ (∀𝑥∀𝑦(𝑥 ⊆ 𝑦 ↔ (𝑥 ∪ (𝑦 ∖ 𝑥)) = 𝑦) → (𝑧 ⊆ {∅} → DECID ∅ ∈ 𝑧))
48	47	alrimiv 1874	. . 3 ⊢ (∀𝑥∀𝑦(𝑥 ⊆ 𝑦 ↔ (𝑥 ∪ (𝑦 ∖ 𝑥)) = 𝑦) → ∀𝑧(𝑧 ⊆ {∅} → DECID ∅ ∈ 𝑧))
49		df-exmid 4192	. . 3 ⊢ (EXMID ↔ ∀𝑧(𝑧 ⊆ {∅} → DECID ∅ ∈ 𝑧))
50	48, 49	sylibr 134	. 2 ⊢ (∀𝑥∀𝑦(𝑥 ⊆ 𝑦 ↔ (𝑥 ∪ (𝑦 ∖ 𝑥)) = 𝑦) → EXMID)
51	25, 50	impbii 126	1 ⊢ (EXMID ↔ ∀𝑥∀𝑦(𝑥 ⊆ 𝑦 ↔ (𝑥 ∪ (𝑦 ∖ 𝑥)) = 𝑦))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 104   ↔ wb 105   ∨ wo 708  DECID wdc 834  ∀wal 1351   = wceq 1353   ∈ wcel 2148  Vcvv 2737   ∖ cdif 3126   ∪ cun 3127   ⊆ wss 3129  ∅c0 3422  {csn 3591  EXMIDwem 4191

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 4118  ax-nul 4126  ax-pow 4171

This theorem depends on definitions:  df-bi 117  df-dc 835  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-rab 2464  df-v 2739  df-dif 3131  df-un 3133  df-in 3135  df-ss 3142  df-nul 3423  df-pw 3576  df-sn 3597  df-exmid 4192

This theorem is referenced by: (None)