Theorem exmidsssnc 4086

Description: Excluded middle in terms of subsets of a singleton. This is similar to exmid01 4081 but lets you choose any set as the element of the singleton rather than just ∅. It is similar to exmidsssn 4085 but for a particular set 𝐵 rather than all sets. (Contributed by Jim Kingdon, 29-Jul-2023.)

Assertion

Ref	Expression
exmidsssnc	⊢ (𝐵 ∈ 𝑉 → (EXMID ↔ ∀𝑥(𝑥 ⊆ {𝐵} → (𝑥 = ∅ ∨ 𝑥 = {𝐵}))))

Distinct variable groups:   𝑥,𝐵   𝑥,𝑉

Proof of Theorem exmidsssnc

Dummy variables 𝑢 𝑤 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		exmidsssn 4085	. . . 4 ⊢ (EXMID ↔ ∀𝑥∀𝑢(𝑥 ⊆ {𝑢} ↔ (𝑥 = ∅ ∨ 𝑥 = {𝑢})))
2		sneq 3504	. . . . . . . 8 ⊢ (𝑢 = 𝐵 → {𝑢} = {𝐵})
3	2	sseq2d 3093	. . . . . . 7 ⊢ (𝑢 = 𝐵 → (𝑥 ⊆ {𝑢} ↔ 𝑥 ⊆ {𝐵}))
4	2	eqeq2d 2126	. . . . . . . 8 ⊢ (𝑢 = 𝐵 → (𝑥 = {𝑢} ↔ 𝑥 = {𝐵}))
5	4	orbi2d 762	. . . . . . 7 ⊢ (𝑢 = 𝐵 → ((𝑥 = ∅ ∨ 𝑥 = {𝑢}) ↔ (𝑥 = ∅ ∨ 𝑥 = {𝐵})))
6	3, 5	bibi12d 234	. . . . . 6 ⊢ (𝑢 = 𝐵 → ((𝑥 ⊆ {𝑢} ↔ (𝑥 = ∅ ∨ 𝑥 = {𝑢})) ↔ (𝑥 ⊆ {𝐵} ↔ (𝑥 = ∅ ∨ 𝑥 = {𝐵}))))
7	6	spcgv 2744	. . . . 5 ⊢ (𝐵 ∈ 𝑉 → (∀𝑢(𝑥 ⊆ {𝑢} ↔ (𝑥 = ∅ ∨ 𝑥 = {𝑢})) → (𝑥 ⊆ {𝐵} ↔ (𝑥 = ∅ ∨ 𝑥 = {𝐵}))))
8	7	alimdv 1833	. . . 4 ⊢ (𝐵 ∈ 𝑉 → (∀𝑥∀𝑢(𝑥 ⊆ {𝑢} ↔ (𝑥 = ∅ ∨ 𝑥 = {𝑢})) → ∀𝑥(𝑥 ⊆ {𝐵} ↔ (𝑥 = ∅ ∨ 𝑥 = {𝐵}))))
9	1, 8	syl5bi 151	. . 3 ⊢ (𝐵 ∈ 𝑉 → (EXMID → ∀𝑥(𝑥 ⊆ {𝐵} ↔ (𝑥 = ∅ ∨ 𝑥 = {𝐵}))))
10		bi1 117	. . . 4 ⊢ ((𝑥 ⊆ {𝐵} ↔ (𝑥 = ∅ ∨ 𝑥 = {𝐵})) → (𝑥 ⊆ {𝐵} → (𝑥 = ∅ ∨ 𝑥 = {𝐵})))
11	10	alimi 1414	. . 3 ⊢ (∀𝑥(𝑥 ⊆ {𝐵} ↔ (𝑥 = ∅ ∨ 𝑥 = {𝐵})) → ∀𝑥(𝑥 ⊆ {𝐵} → (𝑥 = ∅ ∨ 𝑥 = {𝐵})))
12	9, 11	syl6 33	. 2 ⊢ (𝐵 ∈ 𝑉 → (EXMID → ∀𝑥(𝑥 ⊆ {𝐵} → (𝑥 = ∅ ∨ 𝑥 = {𝐵}))))
13		ssrab2 3148	. . . . . . . . 9 ⊢ {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} ⊆ {𝐵}
14		snexg 4068	. . . . . . . . . 10 ⊢ (𝐵 ∈ 𝑉 → {𝐵} ∈ V)
15		rabexg 4031	. . . . . . . . . 10 ⊢ ({𝐵} ∈ V → {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} ∈ V)
16		sseq1 3086	. . . . . . . . . . . 12 ⊢ (𝑥 = {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} → (𝑥 ⊆ {𝐵} ↔ {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} ⊆ {𝐵}))
17		eqeq1 2121	. . . . . . . . . . . . 13 ⊢ (𝑥 = {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} → (𝑥 = ∅ ↔ {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = ∅))
18		eqeq1 2121	. . . . . . . . . . . . 13 ⊢ (𝑥 = {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} → (𝑥 = {𝐵} ↔ {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = {𝐵}))
19	17, 18	orbi12d 765	. . . . . . . . . . . 12 ⊢ (𝑥 = {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} → ((𝑥 = ∅ ∨ 𝑥 = {𝐵}) ↔ ({𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = ∅ ∨ {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = {𝐵})))
20	16, 19	imbi12d 233	. . . . . . . . . . 11 ⊢ (𝑥 = {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} → ((𝑥 ⊆ {𝐵} → (𝑥 = ∅ ∨ 𝑥 = {𝐵})) ↔ ({𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} ⊆ {𝐵} → ({𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = ∅ ∨ {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = {𝐵}))))
21	20	spcgv 2744	. . . . . . . . . 10 ⊢ ({𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} ∈ V → (∀𝑥(𝑥 ⊆ {𝐵} → (𝑥 = ∅ ∨ 𝑥 = {𝐵})) → ({𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} ⊆ {𝐵} → ({𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = ∅ ∨ {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = {𝐵}))))
22	14, 15, 21	3syl 17	. . . . . . . . 9 ⊢ (𝐵 ∈ 𝑉 → (∀𝑥(𝑥 ⊆ {𝐵} → (𝑥 = ∅ ∨ 𝑥 = {𝐵})) → ({𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} ⊆ {𝐵} → ({𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = ∅ ∨ {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = {𝐵}))))
23	13, 22	mpii 44	. . . . . . . 8 ⊢ (𝐵 ∈ 𝑉 → (∀𝑥(𝑥 ⊆ {𝐵} → (𝑥 = ∅ ∨ 𝑥 = {𝐵})) → ({𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = ∅ ∨ {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = {𝐵})))
24		snmg 3607	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ 𝑉 → ∃𝑤 𝑤 ∈ {𝐵})
25		r19.3rmv 3419	. . . . . . . . . . . 12 ⊢ (∃𝑤 𝑤 ∈ {𝐵} → (¬ ∅ ∈ 𝑦 ↔ ∀𝑧 ∈ {𝐵} ¬ ∅ ∈ 𝑦))
26	24, 25	syl 14	. . . . . . . . . . 11 ⊢ (𝐵 ∈ 𝑉 → (¬ ∅ ∈ 𝑦 ↔ ∀𝑧 ∈ {𝐵} ¬ ∅ ∈ 𝑦))
27		rabeq0 3358	. . . . . . . . . . 11 ⊢ ({𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = ∅ ↔ ∀𝑧 ∈ {𝐵} ¬ ∅ ∈ 𝑦)
28	26, 27	syl6rbbr 198	. . . . . . . . . 10 ⊢ (𝐵 ∈ 𝑉 → ({𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = ∅ ↔ ¬ ∅ ∈ 𝑦))
29	28	biimpd 143	. . . . . . . . 9 ⊢ (𝐵 ∈ 𝑉 → ({𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = ∅ → ¬ ∅ ∈ 𝑦))
30		snidg 3520	. . . . . . . . . . . . 13 ⊢ (𝐵 ∈ 𝑉 → 𝐵 ∈ {𝐵})
31	30	adantr 272	. . . . . . . . . . . 12 ⊢ ((𝐵 ∈ 𝑉 ∧ {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = {𝐵}) → 𝐵 ∈ {𝐵})
32		simpr 109	. . . . . . . . . . . 12 ⊢ ((𝐵 ∈ 𝑉 ∧ {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = {𝐵}) → {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = {𝐵})
33	31, 32	eleqtrrd 2194	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ 𝑉 ∧ {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = {𝐵}) → 𝐵 ∈ {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦})
34		biidd 171	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝐵 → (∅ ∈ 𝑦 ↔ ∅ ∈ 𝑦))
35	34	elrab 2809	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} ↔ (𝐵 ∈ {𝐵} ∧ ∅ ∈ 𝑦))
36	35	simprbi 271	. . . . . . . . . . 11 ⊢ (𝐵 ∈ {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} → ∅ ∈ 𝑦)
37	33, 36	syl 14	. . . . . . . . . 10 ⊢ ((𝐵 ∈ 𝑉 ∧ {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = {𝐵}) → ∅ ∈ 𝑦)
38	37	ex 114	. . . . . . . . 9 ⊢ (𝐵 ∈ 𝑉 → ({𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = {𝐵} → ∅ ∈ 𝑦))
39	29, 38	orim12d 758	. . . . . . . 8 ⊢ (𝐵 ∈ 𝑉 → (({𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = ∅ ∨ {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = {𝐵}) → (¬ ∅ ∈ 𝑦 ∨ ∅ ∈ 𝑦)))
40	23, 39	syld 45	. . . . . . 7 ⊢ (𝐵 ∈ 𝑉 → (∀𝑥(𝑥 ⊆ {𝐵} → (𝑥 = ∅ ∨ 𝑥 = {𝐵})) → (¬ ∅ ∈ 𝑦 ∨ ∅ ∈ 𝑦)))
41		orcom 700	. . . . . . 7 ⊢ ((¬ ∅ ∈ 𝑦 ∨ ∅ ∈ 𝑦) ↔ (∅ ∈ 𝑦 ∨ ¬ ∅ ∈ 𝑦))
42	40, 41	syl6ib 160	. . . . . 6 ⊢ (𝐵 ∈ 𝑉 → (∀𝑥(𝑥 ⊆ {𝐵} → (𝑥 = ∅ ∨ 𝑥 = {𝐵})) → (∅ ∈ 𝑦 ∨ ¬ ∅ ∈ 𝑦)))
43		df-dc 803	. . . . . 6 ⊢ (DECID ∅ ∈ 𝑦 ↔ (∅ ∈ 𝑦 ∨ ¬ ∅ ∈ 𝑦))
44	42, 43	syl6ibr 161	. . . . 5 ⊢ (𝐵 ∈ 𝑉 → (∀𝑥(𝑥 ⊆ {𝐵} → (𝑥 = ∅ ∨ 𝑥 = {𝐵})) → DECID ∅ ∈ 𝑦))
45	44	a1dd 48	. . . 4 ⊢ (𝐵 ∈ 𝑉 → (∀𝑥(𝑥 ⊆ {𝐵} → (𝑥 = ∅ ∨ 𝑥 = {𝐵})) → (𝑦 ⊆ {∅} → DECID ∅ ∈ 𝑦)))
46	45	alrimdv 1830	. . 3 ⊢ (𝐵 ∈ 𝑉 → (∀𝑥(𝑥 ⊆ {𝐵} → (𝑥 = ∅ ∨ 𝑥 = {𝐵})) → ∀𝑦(𝑦 ⊆ {∅} → DECID ∅ ∈ 𝑦)))
47		df-exmid 4079	. . 3 ⊢ (EXMID ↔ ∀𝑦(𝑦 ⊆ {∅} → DECID ∅ ∈ 𝑦))
48	46, 47	syl6ibr 161	. 2 ⊢ (𝐵 ∈ 𝑉 → (∀𝑥(𝑥 ⊆ {𝐵} → (𝑥 = ∅ ∨ 𝑥 = {𝐵})) → EXMID))
49	12, 48	impbid 128	1 ⊢ (𝐵 ∈ 𝑉 → (EXMID ↔ ∀𝑥(𝑥 ⊆ {𝐵} → (𝑥 = ∅ ∨ 𝑥 = {𝐵}))))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 103   ↔ wb 104   ∨ wo 680  DECID wdc 802  ∀wal 1312   = wceq 1314  ∃wex 1451   ∈ wcel 1463  ∀wral 2390  {crab 2394  Vcvv 2657   ⊆ wss 3037  ∅c0 3329  {csn 3493  EXMIDwem 4078

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 586  ax-in2 587  ax-io 681  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-10 1466  ax-11 1467  ax-i12 1468  ax-bndl 1469  ax-4 1470  ax-14 1475  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097  ax-sep 4006  ax-nul 4014  ax-pow 4058

This theorem depends on definitions:  df-bi 116  df-dc 803  df-tru 1317  df-fal 1320  df-nf 1420  df-sb 1719  df-clab 2102  df-cleq 2108  df-clel 2111  df-nfc 2244  df-ne 2283  df-ral 2395  df-rab 2399  df-v 2659  df-dif 3039  df-in 3043  df-ss 3050  df-nul 3330  df-pw 3478  df-sn 3499  df-exmid 4079

This theorem is referenced by:  exmidunben  11784