Theorem exmidundifim 4240

Description: Excluded middle is equivalent to every subset having a complement. Variation of exmidundif 4239 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 3531	. . . . . . 7 ⊢ (𝑥 ⊆ 𝑦 ↔ (𝑥 ∪ (𝑦 ∖ 𝑥)) ⊆ 𝑦)
2	1	biimpi 120	. . . . . 6 ⊢ (𝑥 ⊆ 𝑦 → (𝑥 ∪ (𝑦 ∖ 𝑥)) ⊆ 𝑦)
3	2	adantl 277	. . . . 5 ⊢ ((EXMID ∧ 𝑥 ⊆ 𝑦) → (𝑥 ∪ (𝑦 ∖ 𝑥)) ⊆ 𝑦)
4		elun1 3330	. . . . . . . . . 10 ⊢ (𝑧 ∈ 𝑥 → 𝑧 ∈ (𝑥 ∪ (𝑦 ∖ 𝑥)))
5	4	adantl 277	. . . . . . . . 9 ⊢ (((EXMID ∧ 𝑧 ∈ 𝑦) ∧ 𝑧 ∈ 𝑥) → 𝑧 ∈ (𝑥 ∪ (𝑦 ∖ 𝑥)))
6		simplr 528	. . . . . . . . . . 11 ⊢ (((EXMID ∧ 𝑧 ∈ 𝑦) ∧ ¬ 𝑧 ∈ 𝑥) → 𝑧 ∈ 𝑦)
7		simpr 110	. . . . . . . . . . 11 ⊢ (((EXMID ∧ 𝑧 ∈ 𝑦) ∧ ¬ 𝑧 ∈ 𝑥) → ¬ 𝑧 ∈ 𝑥)
8	6, 7	eldifd 3167	. . . . . . . . . 10 ⊢ (((EXMID ∧ 𝑧 ∈ 𝑦) ∧ ¬ 𝑧 ∈ 𝑥) → 𝑧 ∈ (𝑦 ∖ 𝑥))
9		elun2 3331	. . . . . . . . . 10 ⊢ (𝑧 ∈ (𝑦 ∖ 𝑥) → 𝑧 ∈ (𝑥 ∪ (𝑦 ∖ 𝑥)))
10	8, 9	syl 14	. . . . . . . . 9 ⊢ (((EXMID ∧ 𝑧 ∈ 𝑦) ∧ ¬ 𝑧 ∈ 𝑥) → 𝑧 ∈ (𝑥 ∪ (𝑦 ∖ 𝑥)))
11		exmidexmid 4229	. . . . . . . . . . 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 3189	. . . . . 6 ⊢ (EXMID → 𝑦 ⊆ (𝑥 ∪ (𝑦 ∖ 𝑥)))
18	17	adantr 276	. . . . 5 ⊢ ((EXMID ∧ 𝑥 ⊆ 𝑦) → 𝑦 ⊆ (𝑥 ∪ (𝑦 ∖ 𝑥)))
19	3, 18	eqssd 3200	. . . 4 ⊢ ((EXMID ∧ 𝑥 ⊆ 𝑦) → (𝑥 ∪ (𝑦 ∖ 𝑥)) = 𝑦)
20	19	ex 115	. . 3 ⊢ (EXMID → (𝑥 ⊆ 𝑦 → (𝑥 ∪ (𝑦 ∖ 𝑥)) = 𝑦))
21	20	alrimivv 1889	. 2 ⊢ (EXMID → ∀𝑥∀𝑦(𝑥 ⊆ 𝑦 → (𝑥 ∪ (𝑦 ∖ 𝑥)) = 𝑦))
22		vex 2766	. . . . . 6 ⊢ 𝑧 ∈ V
23		p0ex 4221	. . . . . 6 ⊢ {∅} ∈ V
24		sseq12 3208	. . . . . . . 8 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = {∅}) → (𝑥 ⊆ 𝑦 ↔ 𝑧 ⊆ {∅}))
25		simpl 109	. . . . . . . . . 10 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = {∅}) → 𝑥 = 𝑧)
26		simpr 110	. . . . . . . . . . 11 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = {∅}) → 𝑦 = {∅})
27	26, 25	difeq12d 3282	. . . . . . . . . 10 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = {∅}) → (𝑦 ∖ 𝑥) = ({∅} ∖ 𝑧))
28	25, 27	uneq12d 3318	. . . . . . . . 9 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = {∅}) → (𝑥 ∪ (𝑦 ∖ 𝑥)) = (𝑧 ∪ ({∅} ∖ 𝑧)))
29	28, 26	eqeq12d 2211	. . . . . . . 8 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = {∅}) → ((𝑥 ∪ (𝑦 ∖ 𝑥)) = 𝑦 ↔ (𝑧 ∪ ({∅} ∖ 𝑧)) = {∅}))
30	24, 29	imbi12d 234	. . . . . . 7 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = {∅}) → ((𝑥 ⊆ 𝑦 → (𝑥 ∪ (𝑦 ∖ 𝑥)) = 𝑦) ↔ (𝑧 ⊆ {∅} → (𝑧 ∪ ({∅} ∖ 𝑧)) = {∅})))
31	30	spc2gv 2855	. . . . . 6 ⊢ ((𝑧 ∈ V ∧ {∅} ∈ V) → (∀𝑥∀𝑦(𝑥 ⊆ 𝑦 → (𝑥 ∪ (𝑦 ∖ 𝑥)) = 𝑦) → (𝑧 ⊆ {∅} → (𝑧 ∪ ({∅} ∖ 𝑧)) = {∅})))
32	22, 23, 31	mp2an 426	. . . . 5 ⊢ (∀𝑥∀𝑦(𝑥 ⊆ 𝑦 → (𝑥 ∪ (𝑦 ∖ 𝑥)) = 𝑦) → (𝑧 ⊆ {∅} → (𝑧 ∪ ({∅} ∖ 𝑧)) = {∅}))
33		0ex 4160	. . . . . . . 8 ⊢ ∅ ∈ V
34	33	snid 3653	. . . . . . 7 ⊢ ∅ ∈ {∅}
35		eleq2 2260	. . . . . . 7 ⊢ ((𝑧 ∪ ({∅} ∖ 𝑧)) = {∅} → (∅ ∈ (𝑧 ∪ ({∅} ∖ 𝑧)) ↔ ∅ ∈ {∅}))
36	34, 35	mpbiri 168	. . . . . 6 ⊢ ((𝑧 ∪ ({∅} ∖ 𝑧)) = {∅} → ∅ ∈ (𝑧 ∪ ({∅} ∖ 𝑧)))
37		eldifn 3286	. . . . . . . 8 ⊢ (∅ ∈ ({∅} ∖ 𝑧) → ¬ ∅ ∈ 𝑧)
38	37	orim2i 762	. . . . . . 7 ⊢ ((∅ ∈ 𝑧 ∨ ∅ ∈ ({∅} ∖ 𝑧)) → (∅ ∈ 𝑧 ∨ ¬ ∅ ∈ 𝑧))
39		elun 3304	. . . . . . 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 1888	. . 3 ⊢ (∀𝑥∀𝑦(𝑥 ⊆ 𝑦 → (𝑥 ∪ (𝑦 ∖ 𝑥)) = 𝑦) → ∀𝑧(𝑧 ⊆ {∅} → DECID ∅ ∈ 𝑧))
45		df-exmid 4228	. . 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 2167  Vcvv 2763   ∖ cdif 3154   ∪ cun 3155   ⊆ wss 3157  ∅c0 3450  {csn 3622  EXMIDwem 4227

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-14 2170  ax-ext 2178  ax-sep 4151  ax-nul 4159  ax-pow 4207

This theorem depends on definitions:  df-bi 117  df-dc 836  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-ral 2480  df-rab 2484  df-v 2765  df-dif 3159  df-un 3161  df-in 3163  df-ss 3170  df-nul 3451  df-pw 3607  df-sn 3628  df-exmid 4228

This theorem is referenced by: (None)