Theorem exmidundifim 4303

Description: Excluded middle is equivalent to every subset having a complement. Variation of exmidundif 4302 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 3577	. . . . . . 7 ⊢ (𝑥 ⊆ 𝑦 ↔ (𝑥 ∪ (𝑦 ∖ 𝑥)) ⊆ 𝑦)
2	1	biimpi 120	. . . . . 6 ⊢ (𝑥 ⊆ 𝑦 → (𝑥 ∪ (𝑦 ∖ 𝑥)) ⊆ 𝑦)
3	2	adantl 277	. . . . 5 ⊢ ((EXMID ∧ 𝑥 ⊆ 𝑦) → (𝑥 ∪ (𝑦 ∖ 𝑥)) ⊆ 𝑦)
4		elun1 3376	. . . . . . . . . 10 ⊢ (𝑧 ∈ 𝑥 → 𝑧 ∈ (𝑥 ∪ (𝑦 ∖ 𝑥)))
5	4	adantl 277	. . . . . . . . 9 ⊢ (((EXMID ∧ 𝑧 ∈ 𝑦) ∧ 𝑧 ∈ 𝑥) → 𝑧 ∈ (𝑥 ∪ (𝑦 ∖ 𝑥)))
6		simplr 529	. . . . . . . . . . 11 ⊢ (((EXMID ∧ 𝑧 ∈ 𝑦) ∧ ¬ 𝑧 ∈ 𝑥) → 𝑧 ∈ 𝑦)
7		simpr 110	. . . . . . . . . . 11 ⊢ (((EXMID ∧ 𝑧 ∈ 𝑦) ∧ ¬ 𝑧 ∈ 𝑥) → ¬ 𝑧 ∈ 𝑥)
8	6, 7	eldifd 3211	. . . . . . . . . 10 ⊢ (((EXMID ∧ 𝑧 ∈ 𝑦) ∧ ¬ 𝑧 ∈ 𝑥) → 𝑧 ∈ (𝑦 ∖ 𝑥))
9		elun2 3377	. . . . . . . . . 10 ⊢ (𝑧 ∈ (𝑦 ∖ 𝑥) → 𝑧 ∈ (𝑥 ∪ (𝑦 ∖ 𝑥)))
10	8, 9	syl 14	. . . . . . . . 9 ⊢ (((EXMID ∧ 𝑧 ∈ 𝑦) ∧ ¬ 𝑧 ∈ 𝑥) → 𝑧 ∈ (𝑥 ∪ (𝑦 ∖ 𝑥)))
11		exmidexmid 4292	. . . . . . . . . . 11 ⊢ (EXMID → DECID 𝑧 ∈ 𝑥)
12		exmiddc 844	. . . . . . . . . . 11 ⊢ (DECID 𝑧 ∈ 𝑥 → (𝑧 ∈ 𝑥 ∨ ¬ 𝑧 ∈ 𝑥))
13	11, 12	syl 14	. . . . . . . . . 10 ⊢ (EXMID → (𝑧 ∈ 𝑥 ∨ ¬ 𝑧 ∈ 𝑥))
14	13	adantr 276	. . . . . . . . 9 ⊢ ((EXMID ∧ 𝑧 ∈ 𝑦) → (𝑧 ∈ 𝑥 ∨ ¬ 𝑧 ∈ 𝑥))
15	5, 10, 14	mpjaodan 806	. . . . . . . 8 ⊢ ((EXMID ∧ 𝑧 ∈ 𝑦) → 𝑧 ∈ (𝑥 ∪ (𝑦 ∖ 𝑥)))
16	15	ex 115	. . . . . . 7 ⊢ (EXMID → (𝑧 ∈ 𝑦 → 𝑧 ∈ (𝑥 ∪ (𝑦 ∖ 𝑥))))
17	16	ssrdv 3234	. . . . . 6 ⊢ (EXMID → 𝑦 ⊆ (𝑥 ∪ (𝑦 ∖ 𝑥)))
18	17	adantr 276	. . . . 5 ⊢ ((EXMID ∧ 𝑥 ⊆ 𝑦) → 𝑦 ⊆ (𝑥 ∪ (𝑦 ∖ 𝑥)))
19	3, 18	eqssd 3245	. . . 4 ⊢ ((EXMID ∧ 𝑥 ⊆ 𝑦) → (𝑥 ∪ (𝑦 ∖ 𝑥)) = 𝑦)
20	19	ex 115	. . 3 ⊢ (EXMID → (𝑥 ⊆ 𝑦 → (𝑥 ∪ (𝑦 ∖ 𝑥)) = 𝑦))
21	20	alrimivv 1923	. 2 ⊢ (EXMID → ∀𝑥∀𝑦(𝑥 ⊆ 𝑦 → (𝑥 ∪ (𝑦 ∖ 𝑥)) = 𝑦))
22		vex 2806	. . . . . 6 ⊢ 𝑧 ∈ V
23		p0ex 4284	. . . . . 6 ⊢ {∅} ∈ V
24		sseq12 3253	. . . . . . . 8 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = {∅}) → (𝑥 ⊆ 𝑦 ↔ 𝑧 ⊆ {∅}))
25		simpl 109	. . . . . . . . . 10 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = {∅}) → 𝑥 = 𝑧)
26		simpr 110	. . . . . . . . . . 11 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = {∅}) → 𝑦 = {∅})
27	26, 25	difeq12d 3328	. . . . . . . . . 10 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = {∅}) → (𝑦 ∖ 𝑥) = ({∅} ∖ 𝑧))
28	25, 27	uneq12d 3364	. . . . . . . . 9 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = {∅}) → (𝑥 ∪ (𝑦 ∖ 𝑥)) = (𝑧 ∪ ({∅} ∖ 𝑧)))
29	28, 26	eqeq12d 2246	. . . . . . . 8 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = {∅}) → ((𝑥 ∪ (𝑦 ∖ 𝑥)) = 𝑦 ↔ (𝑧 ∪ ({∅} ∖ 𝑧)) = {∅}))
30	24, 29	imbi12d 234	. . . . . . 7 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = {∅}) → ((𝑥 ⊆ 𝑦 → (𝑥 ∪ (𝑦 ∖ 𝑥)) = 𝑦) ↔ (𝑧 ⊆ {∅} → (𝑧 ∪ ({∅} ∖ 𝑧)) = {∅})))
31	30	spc2gv 2898	. . . . . 6 ⊢ ((𝑧 ∈ V ∧ {∅} ∈ V) → (∀𝑥∀𝑦(𝑥 ⊆ 𝑦 → (𝑥 ∪ (𝑦 ∖ 𝑥)) = 𝑦) → (𝑧 ⊆ {∅} → (𝑧 ∪ ({∅} ∖ 𝑧)) = {∅})))
32	22, 23, 31	mp2an 426	. . . . 5 ⊢ (∀𝑥∀𝑦(𝑥 ⊆ 𝑦 → (𝑥 ∪ (𝑦 ∖ 𝑥)) = 𝑦) → (𝑧 ⊆ {∅} → (𝑧 ∪ ({∅} ∖ 𝑧)) = {∅}))
33		0ex 4221	. . . . . . . 8 ⊢ ∅ ∈ V
34	33	snid 3704	. . . . . . 7 ⊢ ∅ ∈ {∅}
35		eleq2 2295	. . . . . . 7 ⊢ ((𝑧 ∪ ({∅} ∖ 𝑧)) = {∅} → (∅ ∈ (𝑧 ∪ ({∅} ∖ 𝑧)) ↔ ∅ ∈ {∅}))
36	34, 35	mpbiri 168	. . . . . 6 ⊢ ((𝑧 ∪ ({∅} ∖ 𝑧)) = {∅} → ∅ ∈ (𝑧 ∪ ({∅} ∖ 𝑧)))
37		eldifn 3332	. . . . . . . 8 ⊢ (∅ ∈ ({∅} ∖ 𝑧) → ¬ ∅ ∈ 𝑧)
38	37	orim2i 769	. . . . . . 7 ⊢ ((∅ ∈ 𝑧 ∨ ∅ ∈ ({∅} ∖ 𝑧)) → (∅ ∈ 𝑧 ∨ ¬ ∅ ∈ 𝑧))
39		elun 3350	. . . . . . 7 ⊢ (∅ ∈ (𝑧 ∪ ({∅} ∖ 𝑧)) ↔ (∅ ∈ 𝑧 ∨ ∅ ∈ ({∅} ∖ 𝑧)))
40		df-dc 843	. . . . . . 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 1922	. . 3 ⊢ (∀𝑥∀𝑦(𝑥 ⊆ 𝑦 → (𝑥 ∪ (𝑦 ∖ 𝑥)) = 𝑦) → ∀𝑧(𝑧 ⊆ {∅} → DECID ∅ ∈ 𝑧))
45		df-exmid 4291	. . 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 716  DECID wdc 842  ∀wal 1396   = wceq 1398   ∈ wcel 2202  Vcvv 2803   ∖ cdif 3198   ∪ cun 3199   ⊆ wss 3201  ∅c0 3496  {csn 3673  EXMIDwem 4290

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 619  ax-in2 620  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-14 2205  ax-ext 2213  ax-sep 4212  ax-nul 4220  ax-pow 4270

This theorem depends on definitions:  df-bi 117  df-dc 843  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-ral 2516  df-rab 2520  df-v 2805  df-dif 3203  df-un 3205  df-in 3207  df-ss 3214  df-nul 3497  df-pw 3658  df-sn 3679  df-exmid 4291

This theorem is referenced by: (None)