Theorem exmidundifim 4236

Description: Excluded middle is equivalent to every subset having a complement. Variation of exmidundif 4235 with an implication rather than a biconditional. (Contributed by Jim Kingdon, 16-Feb-2023.)

Assertion

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

Distinct variable group:   𝑥,𝑦

Proof of Theorem exmidundifim

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		undifss 3527	. . . . . . 7 ⊢ (𝑥 ⊆ 𝑦 ↔ (𝑥 ∪ (𝑦 ∖ 𝑥)) ⊆ 𝑦)
2	1	biimpi 120	. . . . . 6 ⊢ (𝑥 ⊆ 𝑦 → (𝑥 ∪ (𝑦 ∖ 𝑥)) ⊆ 𝑦)
3	2	adantl 277	. . . . 5 ⊢ ((EXMID ∧ 𝑥 ⊆ 𝑦) → (𝑥 ∪ (𝑦 ∖ 𝑥)) ⊆ 𝑦)
4		elun1 3326	. . . . . . . . . 10 ⊢ (𝑧 ∈ 𝑥 → 𝑧 ∈ (𝑥 ∪ (𝑦 ∖ 𝑥)))
5	4	adantl 277	. . . . . . . . 9 ⊢ (((EXMID ∧ 𝑧 ∈ 𝑦) ∧ 𝑧 ∈ 𝑥) → 𝑧 ∈ (𝑥 ∪ (𝑦 ∖ 𝑥)))
6		simplr 528	. . . . . . . . . . 11 ⊢ (((EXMID ∧ 𝑧 ∈ 𝑦) ∧ ¬ 𝑧 ∈ 𝑥) → 𝑧 ∈ 𝑦)
7		simpr 110	. . . . . . . . . . 11 ⊢ (((EXMID ∧ 𝑧 ∈ 𝑦) ∧ ¬ 𝑧 ∈ 𝑥) → ¬ 𝑧 ∈ 𝑥)
8	6, 7	eldifd 3163	. . . . . . . . . 10 ⊢ (((EXMID ∧ 𝑧 ∈ 𝑦) ∧ ¬ 𝑧 ∈ 𝑥) → 𝑧 ∈ (𝑦 ∖ 𝑥))
9		elun2 3327	. . . . . . . . . 10 ⊢ (𝑧 ∈ (𝑦 ∖ 𝑥) → 𝑧 ∈ (𝑥 ∪ (𝑦 ∖ 𝑥)))
10	8, 9	syl 14	. . . . . . . . 9 ⊢ (((EXMID ∧ 𝑧 ∈ 𝑦) ∧ ¬ 𝑧 ∈ 𝑥) → 𝑧 ∈ (𝑥 ∪ (𝑦 ∖ 𝑥)))
11		exmidexmid 4225	. . . . . . . . . . 11 ⊢ (EXMID → DECID 𝑧 ∈ 𝑥)
12		exmiddc 837	. . . . . . . . . . 11 ⊢ (DECID 𝑧 ∈ 𝑥 → (𝑧 ∈ 𝑥 ∨ ¬ 𝑧 ∈ 𝑥))
13	11, 12	syl 14	. . . . . . . . . 10 ⊢ (EXMID → (𝑧 ∈ 𝑥 ∨ ¬ 𝑧 ∈ 𝑥))
14	13	adantr 276	. . . . . . . . 9 ⊢ ((EXMID ∧ 𝑧 ∈ 𝑦) → (𝑧 ∈ 𝑥 ∨ ¬ 𝑧 ∈ 𝑥))
15	5, 10, 14	mpjaodan 799	. . . . . . . 8 ⊢ ((EXMID ∧ 𝑧 ∈ 𝑦) → 𝑧 ∈ (𝑥 ∪ (𝑦 ∖ 𝑥)))
16	15	ex 115	. . . . . . 7 ⊢ (EXMID → (𝑧 ∈ 𝑦 → 𝑧 ∈ (𝑥 ∪ (𝑦 ∖ 𝑥))))
17	16	ssrdv 3185	. . . . . 6 ⊢ (EXMID → 𝑦 ⊆ (𝑥 ∪ (𝑦 ∖ 𝑥)))
18	17	adantr 276	. . . . 5 ⊢ ((EXMID ∧ 𝑥 ⊆ 𝑦) → 𝑦 ⊆ (𝑥 ∪ (𝑦 ∖ 𝑥)))
19	3, 18	eqssd 3196	. . . 4 ⊢ ((EXMID ∧ 𝑥 ⊆ 𝑦) → (𝑥 ∪ (𝑦 ∖ 𝑥)) = 𝑦)
20	19	ex 115	. . 3 ⊢ (EXMID → (𝑥 ⊆ 𝑦 → (𝑥 ∪ (𝑦 ∖ 𝑥)) = 𝑦))
21	20	alrimivv 1886	. 2 ⊢ (EXMID → ∀𝑥∀𝑦(𝑥 ⊆ 𝑦 → (𝑥 ∪ (𝑦 ∖ 𝑥)) = 𝑦))
22		vex 2763	. . . . . 6 ⊢ 𝑧 ∈ V
23		p0ex 4217	. . . . . 6 ⊢ {∅} ∈ V
24		sseq12 3204	. . . . . . . 8 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = {∅}) → (𝑥 ⊆ 𝑦 ↔ 𝑧 ⊆ {∅}))
25		simpl 109	. . . . . . . . . 10 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = {∅}) → 𝑥 = 𝑧)
26		simpr 110	. . . . . . . . . . 11 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = {∅}) → 𝑦 = {∅})
27	26, 25	difeq12d 3278	. . . . . . . . . 10 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = {∅}) → (𝑦 ∖ 𝑥) = ({∅} ∖ 𝑧))
28	25, 27	uneq12d 3314	. . . . . . . . 9 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = {∅}) → (𝑥 ∪ (𝑦 ∖ 𝑥)) = (𝑧 ∪ ({∅} ∖ 𝑧)))
29	28, 26	eqeq12d 2208	. . . . . . . 8 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = {∅}) → ((𝑥 ∪ (𝑦 ∖ 𝑥)) = 𝑦 ↔ (𝑧 ∪ ({∅} ∖ 𝑧)) = {∅}))
30	24, 29	imbi12d 234	. . . . . . 7 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = {∅}) → ((𝑥 ⊆ 𝑦 → (𝑥 ∪ (𝑦 ∖ 𝑥)) = 𝑦) ↔ (𝑧 ⊆ {∅} → (𝑧 ∪ ({∅} ∖ 𝑧)) = {∅})))
31	30	spc2gv 2851	. . . . . 6 ⊢ ((𝑧 ∈ V ∧ {∅} ∈ V) → (∀𝑥∀𝑦(𝑥 ⊆ 𝑦 → (𝑥 ∪ (𝑦 ∖ 𝑥)) = 𝑦) → (𝑧 ⊆ {∅} → (𝑧 ∪ ({∅} ∖ 𝑧)) = {∅})))
32	22, 23, 31	mp2an 426	. . . . 5 ⊢ (∀𝑥∀𝑦(𝑥 ⊆ 𝑦 → (𝑥 ∪ (𝑦 ∖ 𝑥)) = 𝑦) → (𝑧 ⊆ {∅} → (𝑧 ∪ ({∅} ∖ 𝑧)) = {∅}))
33		0ex 4156	. . . . . . . 8 ⊢ ∅ ∈ V
34	33	snid 3649	. . . . . . 7 ⊢ ∅ ∈ {∅}
35		eleq2 2257	. . . . . . 7 ⊢ ((𝑧 ∪ ({∅} ∖ 𝑧)) = {∅} → (∅ ∈ (𝑧 ∪ ({∅} ∖ 𝑧)) ↔ ∅ ∈ {∅}))
36	34, 35	mpbiri 168	. . . . . 6 ⊢ ((𝑧 ∪ ({∅} ∖ 𝑧)) = {∅} → ∅ ∈ (𝑧 ∪ ({∅} ∖ 𝑧)))
37		eldifn 3282	. . . . . . . 8 ⊢ (∅ ∈ ({∅} ∖ 𝑧) → ¬ ∅ ∈ 𝑧)
38	37	orim2i 762	. . . . . . 7 ⊢ ((∅ ∈ 𝑧 ∨ ∅ ∈ ({∅} ∖ 𝑧)) → (∅ ∈ 𝑧 ∨ ¬ ∅ ∈ 𝑧))
39		elun 3300	. . . . . . 7 ⊢ (∅ ∈ (𝑧 ∪ ({∅} ∖ 𝑧)) ↔ (∅ ∈ 𝑧 ∨ ∅ ∈ ({∅} ∖ 𝑧)))
40		df-dc 836	. . . . . . 7 ⊢ (DECID ∅ ∈ 𝑧 ↔ (∅ ∈ 𝑧 ∨ ¬ ∅ ∈ 𝑧))
41	38, 39, 40	3imtr4i 201	. . . . . 6 ⊢ (∅ ∈ (𝑧 ∪ ({∅} ∖ 𝑧)) → DECID ∅ ∈ 𝑧)
42	36, 41	syl 14	. . . . 5 ⊢ ((𝑧 ∪ ({∅} ∖ 𝑧)) = {∅} → DECID ∅ ∈ 𝑧)
43	32, 42	syl6 33	. . . 4 ⊢ (∀𝑥∀𝑦(𝑥 ⊆ 𝑦 → (𝑥 ∪ (𝑦 ∖ 𝑥)) = 𝑦) → (𝑧 ⊆ {∅} → DECID ∅ ∈ 𝑧))
44	43	alrimiv 1885	. . 3 ⊢ (∀𝑥∀𝑦(𝑥 ⊆ 𝑦 → (𝑥 ∪ (𝑦 ∖ 𝑥)) = 𝑦) → ∀𝑧(𝑧 ⊆ {∅} → DECID ∅ ∈ 𝑧))
45		df-exmid 4224	. . 3 ⊢ (EXMID ↔ ∀𝑧(𝑧 ⊆ {∅} → DECID ∅ ∈ 𝑧))
46	44, 45	sylibr 134	. 2 ⊢ (∀𝑥∀𝑦(𝑥 ⊆ 𝑦 → (𝑥 ∪ (𝑦 ∖ 𝑥)) = 𝑦) → EXMID)
47	21, 46	impbii 126	1 ⊢ (EXMID ↔ ∀𝑥∀𝑦(𝑥 ⊆ 𝑦 → (𝑥 ∪ (𝑦 ∖ 𝑥)) = 𝑦))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 104   ↔ wb 105   ∨ wo 709  DECID wdc 835  ∀wal 1362   = wceq 1364   ∈ wcel 2164  Vcvv 2760   ∖ cdif 3150   ∪ cun 3151   ⊆ wss 3153  ∅c0 3446  {csn 3618  EXMIDwem 4223

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-14 2167  ax-ext 2175  ax-sep 4147  ax-nul 4155  ax-pow 4203

This theorem depends on definitions:  df-bi 117  df-dc 836  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ral 2477  df-rab 2481  df-v 2762  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3447  df-pw 3603  df-sn 3624  df-exmid 4224

This theorem is referenced by: (None)