Theorem exmidsssnc 4218

Description: Excluded middle in terms of subsets of a singleton. This is similar to exmid01 4213 but lets you choose any set as the element of the singleton rather than just ∅. It is similar to exmidsssn 4217 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 4217	. . . 4 ⊢ (EXMID ↔ ∀𝑥∀𝑢(𝑥 ⊆ {𝑢} ↔ (𝑥 = ∅ ∨ 𝑥 = {𝑢})))
2		sneq 3618	. . . . . . . 8 ⊢ (𝑢 = 𝐵 → {𝑢} = {𝐵})
3	2	sseq2d 3200	. . . . . . 7 ⊢ (𝑢 = 𝐵 → (𝑥 ⊆ {𝑢} ↔ 𝑥 ⊆ {𝐵}))
4	2	eqeq2d 2201	. . . . . . . 8 ⊢ (𝑢 = 𝐵 → (𝑥 = {𝑢} ↔ 𝑥 = {𝐵}))
5	4	orbi2d 791	. . . . . . 7 ⊢ (𝑢 = 𝐵 → ((𝑥 = ∅ ∨ 𝑥 = {𝑢}) ↔ (𝑥 = ∅ ∨ 𝑥 = {𝐵})))
6	3, 5	bibi12d 235	. . . . . 6 ⊢ (𝑢 = 𝐵 → ((𝑥 ⊆ {𝑢} ↔ (𝑥 = ∅ ∨ 𝑥 = {𝑢})) ↔ (𝑥 ⊆ {𝐵} ↔ (𝑥 = ∅ ∨ 𝑥 = {𝐵}))))
7	6	spcgv 2839	. . . . 5 ⊢ (𝐵 ∈ 𝑉 → (∀𝑢(𝑥 ⊆ {𝑢} ↔ (𝑥 = ∅ ∨ 𝑥 = {𝑢})) → (𝑥 ⊆ {𝐵} ↔ (𝑥 = ∅ ∨ 𝑥 = {𝐵}))))
8	7	alimdv 1890	. . . 4 ⊢ (𝐵 ∈ 𝑉 → (∀𝑥∀𝑢(𝑥 ⊆ {𝑢} ↔ (𝑥 = ∅ ∨ 𝑥 = {𝑢})) → ∀𝑥(𝑥 ⊆ {𝐵} ↔ (𝑥 = ∅ ∨ 𝑥 = {𝐵}))))
9	1, 8	biimtrid 152	. . 3 ⊢ (𝐵 ∈ 𝑉 → (EXMID → ∀𝑥(𝑥 ⊆ {𝐵} ↔ (𝑥 = ∅ ∨ 𝑥 = {𝐵}))))
10		biimp 118	. . . 4 ⊢ ((𝑥 ⊆ {𝐵} ↔ (𝑥 = ∅ ∨ 𝑥 = {𝐵})) → (𝑥 ⊆ {𝐵} → (𝑥 = ∅ ∨ 𝑥 = {𝐵})))
11	10	alimi 1466	. . 3 ⊢ (∀𝑥(𝑥 ⊆ {𝐵} ↔ (𝑥 = ∅ ∨ 𝑥 = {𝐵})) → ∀𝑥(𝑥 ⊆ {𝐵} → (𝑥 = ∅ ∨ 𝑥 = {𝐵})))
12	9, 11	syl6 33	. 2 ⊢ (𝐵 ∈ 𝑉 → (EXMID → ∀𝑥(𝑥 ⊆ {𝐵} → (𝑥 = ∅ ∨ 𝑥 = {𝐵}))))
13		ssrab2 3255	. . . . . . . . 9 ⊢ {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} ⊆ {𝐵}
14		snexg 4199	. . . . . . . . . 10 ⊢ (𝐵 ∈ 𝑉 → {𝐵} ∈ V)
15		rabexg 4161	. . . . . . . . . 10 ⊢ ({𝐵} ∈ V → {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} ∈ V)
16		sseq1 3193	. . . . . . . . . . . 12 ⊢ (𝑥 = {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} → (𝑥 ⊆ {𝐵} ↔ {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} ⊆ {𝐵}))
17		eqeq1 2196	. . . . . . . . . . . . 13 ⊢ (𝑥 = {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} → (𝑥 = ∅ ↔ {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = ∅))
18		eqeq1 2196	. . . . . . . . . . . . 13 ⊢ (𝑥 = {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} → (𝑥 = {𝐵} ↔ {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = {𝐵}))
19	17, 18	orbi12d 794	. . . . . . . . . . . 12 ⊢ (𝑥 = {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} → ((𝑥 = ∅ ∨ 𝑥 = {𝐵}) ↔ ({𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = ∅ ∨ {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = {𝐵})))
20	16, 19	imbi12d 234	. . . . . . . . . . 11 ⊢ (𝑥 = {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} → ((𝑥 ⊆ {𝐵} → (𝑥 = ∅ ∨ 𝑥 = {𝐵})) ↔ ({𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} ⊆ {𝐵} → ({𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = ∅ ∨ {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = {𝐵}))))
21	20	spcgv 2839	. . . . . . . . . 10 ⊢ ({𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} ∈ V → (∀𝑥(𝑥 ⊆ {𝐵} → (𝑥 = ∅ ∨ 𝑥 = {𝐵})) → ({𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} ⊆ {𝐵} → ({𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = ∅ ∨ {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = {𝐵}))))
22	14, 15, 21	3syl 17	. . . . . . . . 9 ⊢ (𝐵 ∈ 𝑉 → (∀𝑥(𝑥 ⊆ {𝐵} → (𝑥 = ∅ ∨ 𝑥 = {𝐵})) → ({𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} ⊆ {𝐵} → ({𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = ∅ ∨ {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = {𝐵}))))
23	13, 22	mpii 44	. . . . . . . 8 ⊢ (𝐵 ∈ 𝑉 → (∀𝑥(𝑥 ⊆ {𝐵} → (𝑥 = ∅ ∨ 𝑥 = {𝐵})) → ({𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = ∅ ∨ {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = {𝐵})))
24		rabeq0 3467	. . . . . . . . . . 11 ⊢ ({𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = ∅ ↔ ∀𝑧 ∈ {𝐵} ¬ ∅ ∈ 𝑦)
25		snmg 3725	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ 𝑉 → ∃𝑤 𝑤 ∈ {𝐵})
26		r19.3rmv 3528	. . . . . . . . . . . 12 ⊢ (∃𝑤 𝑤 ∈ {𝐵} → (¬ ∅ ∈ 𝑦 ↔ ∀𝑧 ∈ {𝐵} ¬ ∅ ∈ 𝑦))
27	25, 26	syl 14	. . . . . . . . . . 11 ⊢ (𝐵 ∈ 𝑉 → (¬ ∅ ∈ 𝑦 ↔ ∀𝑧 ∈ {𝐵} ¬ ∅ ∈ 𝑦))
28	24, 27	bitr4id 199	. . . . . . . . . 10 ⊢ (𝐵 ∈ 𝑉 → ({𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = ∅ ↔ ¬ ∅ ∈ 𝑦))
29	28	biimpd 144	. . . . . . . . 9 ⊢ (𝐵 ∈ 𝑉 → ({𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = ∅ → ¬ ∅ ∈ 𝑦))
30		snidg 3636	. . . . . . . . . . . . 13 ⊢ (𝐵 ∈ 𝑉 → 𝐵 ∈ {𝐵})
31	30	adantr 276	. . . . . . . . . . . 12 ⊢ ((𝐵 ∈ 𝑉 ∧ {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = {𝐵}) → 𝐵 ∈ {𝐵})
32		simpr 110	. . . . . . . . . . . 12 ⊢ ((𝐵 ∈ 𝑉 ∧ {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = {𝐵}) → {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = {𝐵})
33	31, 32	eleqtrrd 2269	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ 𝑉 ∧ {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = {𝐵}) → 𝐵 ∈ {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦})
34		biidd 172	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝐵 → (∅ ∈ 𝑦 ↔ ∅ ∈ 𝑦))
35	34	elrab 2908	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} ↔ (𝐵 ∈ {𝐵} ∧ ∅ ∈ 𝑦))
36	35	simprbi 275	. . . . . . . . . . 11 ⊢ (𝐵 ∈ {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} → ∅ ∈ 𝑦)
37	33, 36	syl 14	. . . . . . . . . 10 ⊢ ((𝐵 ∈ 𝑉 ∧ {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = {𝐵}) → ∅ ∈ 𝑦)
38	37	ex 115	. . . . . . . . 9 ⊢ (𝐵 ∈ 𝑉 → ({𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = {𝐵} → ∅ ∈ 𝑦))
39	29, 38	orim12d 787	. . . . . . . 8 ⊢ (𝐵 ∈ 𝑉 → (({𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = ∅ ∨ {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = {𝐵}) → (¬ ∅ ∈ 𝑦 ∨ ∅ ∈ 𝑦)))
40	23, 39	syld 45	. . . . . . 7 ⊢ (𝐵 ∈ 𝑉 → (∀𝑥(𝑥 ⊆ {𝐵} → (𝑥 = ∅ ∨ 𝑥 = {𝐵})) → (¬ ∅ ∈ 𝑦 ∨ ∅ ∈ 𝑦)))
41		orcom 729	. . . . . . 7 ⊢ ((¬ ∅ ∈ 𝑦 ∨ ∅ ∈ 𝑦) ↔ (∅ ∈ 𝑦 ∨ ¬ ∅ ∈ 𝑦))
42	40, 41	imbitrdi 161	. . . . . 6 ⊢ (𝐵 ∈ 𝑉 → (∀𝑥(𝑥 ⊆ {𝐵} → (𝑥 = ∅ ∨ 𝑥 = {𝐵})) → (∅ ∈ 𝑦 ∨ ¬ ∅ ∈ 𝑦)))
43		df-dc 836	. . . . . 6 ⊢ (DECID ∅ ∈ 𝑦 ↔ (∅ ∈ 𝑦 ∨ ¬ ∅ ∈ 𝑦))
44	42, 43	imbitrrdi 162	. . . . 5 ⊢ (𝐵 ∈ 𝑉 → (∀𝑥(𝑥 ⊆ {𝐵} → (𝑥 = ∅ ∨ 𝑥 = {𝐵})) → DECID ∅ ∈ 𝑦))
45	44	a1dd 48	. . . 4 ⊢ (𝐵 ∈ 𝑉 → (∀𝑥(𝑥 ⊆ {𝐵} → (𝑥 = ∅ ∨ 𝑥 = {𝐵})) → (𝑦 ⊆ {∅} → DECID ∅ ∈ 𝑦)))
46	45	alrimdv 1887	. . 3 ⊢ (𝐵 ∈ 𝑉 → (∀𝑥(𝑥 ⊆ {𝐵} → (𝑥 = ∅ ∨ 𝑥 = {𝐵})) → ∀𝑦(𝑦 ⊆ {∅} → DECID ∅ ∈ 𝑦)))
47		df-exmid 4210	. . 3 ⊢ (EXMID ↔ ∀𝑦(𝑦 ⊆ {∅} → DECID ∅ ∈ 𝑦))
48	46, 47	imbitrrdi 162	. 2 ⊢ (𝐵 ∈ 𝑉 → (∀𝑥(𝑥 ⊆ {𝐵} → (𝑥 = ∅ ∨ 𝑥 = {𝐵})) → EXMID))
49	12, 48	impbid 129	1 ⊢ (𝐵 ∈ 𝑉 → (EXMID ↔ ∀𝑥(𝑥 ⊆ {𝐵} → (𝑥 = ∅ ∨ 𝑥 = {𝐵}))))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 104   ↔ wb 105   ∨ wo 709  DECID wdc 835  ∀wal 1362   = wceq 1364  ∃wex 1503   ∈ wcel 2160  ∀wral 2468  {crab 2472  Vcvv 2752   ⊆ wss 3144  ∅c0 3437  {csn 3607  EXMIDwem 4209

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 2163  ax-ext 2171  ax-sep 4136  ax-nul 4144  ax-pow 4189

This theorem depends on definitions:  df-bi 117  df-dc 836  df-tru 1367  df-fal 1370  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-ne 2361  df-ral 2473  df-rab 2477  df-v 2754  df-dif 3146  df-in 3150  df-ss 3157  df-nul 3438  df-pw 3592  df-sn 3613  df-exmid 4210

This theorem is referenced by:  exmidunben  12452