Theorem exmidsssnc 4258

Description: Excluded middle in terms of subsets of a singleton. This is similar to exmid01 4253 but lets you choose any set as the element of the singleton rather than just ∅. It is similar to exmidsssn 4257 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 4257	. . . 4 ⊢ (EXMID ↔ ∀𝑥∀𝑢(𝑥 ⊆ {𝑢} ↔ (𝑥 = ∅ ∨ 𝑥 = {𝑢})))
2		sneq 3649	. . . . . . . 8 ⊢ (𝑢 = 𝐵 → {𝑢} = {𝐵})
3	2	sseq2d 3227	. . . . . . 7 ⊢ (𝑢 = 𝐵 → (𝑥 ⊆ {𝑢} ↔ 𝑥 ⊆ {𝐵}))
4	2	eqeq2d 2218	. . . . . . . 8 ⊢ (𝑢 = 𝐵 → (𝑥 = {𝑢} ↔ 𝑥 = {𝐵}))
5	4	orbi2d 792	. . . . . . 7 ⊢ (𝑢 = 𝐵 → ((𝑥 = ∅ ∨ 𝑥 = {𝑢}) ↔ (𝑥 = ∅ ∨ 𝑥 = {𝐵})))
6	3, 5	bibi12d 235	. . . . . 6 ⊢ (𝑢 = 𝐵 → ((𝑥 ⊆ {𝑢} ↔ (𝑥 = ∅ ∨ 𝑥 = {𝑢})) ↔ (𝑥 ⊆ {𝐵} ↔ (𝑥 = ∅ ∨ 𝑥 = {𝐵}))))
7	6	spcgv 2864	. . . . 5 ⊢ (𝐵 ∈ 𝑉 → (∀𝑢(𝑥 ⊆ {𝑢} ↔ (𝑥 = ∅ ∨ 𝑥 = {𝑢})) → (𝑥 ⊆ {𝐵} ↔ (𝑥 = ∅ ∨ 𝑥 = {𝐵}))))
8	7	alimdv 1903	. . . 4 ⊢ (𝐵 ∈ 𝑉 → (∀𝑥∀𝑢(𝑥 ⊆ {𝑢} ↔ (𝑥 = ∅ ∨ 𝑥 = {𝑢})) → ∀𝑥(𝑥 ⊆ {𝐵} ↔ (𝑥 = ∅ ∨ 𝑥 = {𝐵}))))
9	1, 8	biimtrid 152	. . 3 ⊢ (𝐵 ∈ 𝑉 → (EXMID → ∀𝑥(𝑥 ⊆ {𝐵} ↔ (𝑥 = ∅ ∨ 𝑥 = {𝐵}))))
10		biimp 118	. . . 4 ⊢ ((𝑥 ⊆ {𝐵} ↔ (𝑥 = ∅ ∨ 𝑥 = {𝐵})) → (𝑥 ⊆ {𝐵} → (𝑥 = ∅ ∨ 𝑥 = {𝐵})))
11	10	alimi 1479	. . 3 ⊢ (∀𝑥(𝑥 ⊆ {𝐵} ↔ (𝑥 = ∅ ∨ 𝑥 = {𝐵})) → ∀𝑥(𝑥 ⊆ {𝐵} → (𝑥 = ∅ ∨ 𝑥 = {𝐵})))
12	9, 11	syl6 33	. 2 ⊢ (𝐵 ∈ 𝑉 → (EXMID → ∀𝑥(𝑥 ⊆ {𝐵} → (𝑥 = ∅ ∨ 𝑥 = {𝐵}))))
13		ssrab2 3282	. . . . . . . . 9 ⊢ {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} ⊆ {𝐵}
14		snexg 4239	. . . . . . . . . 10 ⊢ (𝐵 ∈ 𝑉 → {𝐵} ∈ V)
15		rabexg 4198	. . . . . . . . . 10 ⊢ ({𝐵} ∈ V → {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} ∈ V)
16		sseq1 3220	. . . . . . . . . . . 12 ⊢ (𝑥 = {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} → (𝑥 ⊆ {𝐵} ↔ {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} ⊆ {𝐵}))
17		eqeq1 2213	. . . . . . . . . . . . 13 ⊢ (𝑥 = {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} → (𝑥 = ∅ ↔ {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = ∅))
18		eqeq1 2213	. . . . . . . . . . . . 13 ⊢ (𝑥 = {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} → (𝑥 = {𝐵} ↔ {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = {𝐵}))
19	17, 18	orbi12d 795	. . . . . . . . . . . 12 ⊢ (𝑥 = {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} → ((𝑥 = ∅ ∨ 𝑥 = {𝐵}) ↔ ({𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = ∅ ∨ {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = {𝐵})))
20	16, 19	imbi12d 234	. . . . . . . . . . 11 ⊢ (𝑥 = {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} → ((𝑥 ⊆ {𝐵} → (𝑥 = ∅ ∨ 𝑥 = {𝐵})) ↔ ({𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} ⊆ {𝐵} → ({𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = ∅ ∨ {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = {𝐵}))))
21	20	spcgv 2864	. . . . . . . . . 10 ⊢ ({𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} ∈ V → (∀𝑥(𝑥 ⊆ {𝐵} → (𝑥 = ∅ ∨ 𝑥 = {𝐵})) → ({𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} ⊆ {𝐵} → ({𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = ∅ ∨ {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = {𝐵}))))
22	14, 15, 21	3syl 17	. . . . . . . . 9 ⊢ (𝐵 ∈ 𝑉 → (∀𝑥(𝑥 ⊆ {𝐵} → (𝑥 = ∅ ∨ 𝑥 = {𝐵})) → ({𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} ⊆ {𝐵} → ({𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = ∅ ∨ {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = {𝐵}))))
23	13, 22	mpii 44	. . . . . . . 8 ⊢ (𝐵 ∈ 𝑉 → (∀𝑥(𝑥 ⊆ {𝐵} → (𝑥 = ∅ ∨ 𝑥 = {𝐵})) → ({𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = ∅ ∨ {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = {𝐵})))
24		rabeq0 3494	. . . . . . . . . . 11 ⊢ ({𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = ∅ ↔ ∀𝑧 ∈ {𝐵} ¬ ∅ ∈ 𝑦)
25		snmg 3756	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ 𝑉 → ∃𝑤 𝑤 ∈ {𝐵})
26		r19.3rmv 3555	. . . . . . . . . . . 12 ⊢ (∃𝑤 𝑤 ∈ {𝐵} → (¬ ∅ ∈ 𝑦 ↔ ∀𝑧 ∈ {𝐵} ¬ ∅ ∈ 𝑦))
27	25, 26	syl 14	. . . . . . . . . . 11 ⊢ (𝐵 ∈ 𝑉 → (¬ ∅ ∈ 𝑦 ↔ ∀𝑧 ∈ {𝐵} ¬ ∅ ∈ 𝑦))
28	24, 27	bitr4id 199	. . . . . . . . . 10 ⊢ (𝐵 ∈ 𝑉 → ({𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = ∅ ↔ ¬ ∅ ∈ 𝑦))
29	28	biimpd 144	. . . . . . . . 9 ⊢ (𝐵 ∈ 𝑉 → ({𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = ∅ → ¬ ∅ ∈ 𝑦))
30		snidg 3667	. . . . . . . . . . . . 13 ⊢ (𝐵 ∈ 𝑉 → 𝐵 ∈ {𝐵})
31	30	adantr 276	. . . . . . . . . . . 12 ⊢ ((𝐵 ∈ 𝑉 ∧ {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = {𝐵}) → 𝐵 ∈ {𝐵})
32		simpr 110	. . . . . . . . . . . 12 ⊢ ((𝐵 ∈ 𝑉 ∧ {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = {𝐵}) → {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = {𝐵})
33	31, 32	eleqtrrd 2286	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ 𝑉 ∧ {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = {𝐵}) → 𝐵 ∈ {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦})
34		biidd 172	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝐵 → (∅ ∈ 𝑦 ↔ ∅ ∈ 𝑦))
35	34	elrab 2933	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} ↔ (𝐵 ∈ {𝐵} ∧ ∅ ∈ 𝑦))
36	35	simprbi 275	. . . . . . . . . . 11 ⊢ (𝐵 ∈ {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} → ∅ ∈ 𝑦)
37	33, 36	syl 14	. . . . . . . . . 10 ⊢ ((𝐵 ∈ 𝑉 ∧ {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = {𝐵}) → ∅ ∈ 𝑦)
38	37	ex 115	. . . . . . . . 9 ⊢ (𝐵 ∈ 𝑉 → ({𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = {𝐵} → ∅ ∈ 𝑦))
39	29, 38	orim12d 788	. . . . . . . 8 ⊢ (𝐵 ∈ 𝑉 → (({𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = ∅ ∨ {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = {𝐵}) → (¬ ∅ ∈ 𝑦 ∨ ∅ ∈ 𝑦)))
40	23, 39	syld 45	. . . . . . 7 ⊢ (𝐵 ∈ 𝑉 → (∀𝑥(𝑥 ⊆ {𝐵} → (𝑥 = ∅ ∨ 𝑥 = {𝐵})) → (¬ ∅ ∈ 𝑦 ∨ ∅ ∈ 𝑦)))
41		orcom 730	. . . . . . 7 ⊢ ((¬ ∅ ∈ 𝑦 ∨ ∅ ∈ 𝑦) ↔ (∅ ∈ 𝑦 ∨ ¬ ∅ ∈ 𝑦))
42	40, 41	imbitrdi 161	. . . . . 6 ⊢ (𝐵 ∈ 𝑉 → (∀𝑥(𝑥 ⊆ {𝐵} → (𝑥 = ∅ ∨ 𝑥 = {𝐵})) → (∅ ∈ 𝑦 ∨ ¬ ∅ ∈ 𝑦)))
43		df-dc 837	. . . . . 6 ⊢ (DECID ∅ ∈ 𝑦 ↔ (∅ ∈ 𝑦 ∨ ¬ ∅ ∈ 𝑦))
44	42, 43	imbitrrdi 162	. . . . 5 ⊢ (𝐵 ∈ 𝑉 → (∀𝑥(𝑥 ⊆ {𝐵} → (𝑥 = ∅ ∨ 𝑥 = {𝐵})) → DECID ∅ ∈ 𝑦))
45	44	a1dd 48	. . . 4 ⊢ (𝐵 ∈ 𝑉 → (∀𝑥(𝑥 ⊆ {𝐵} → (𝑥 = ∅ ∨ 𝑥 = {𝐵})) → (𝑦 ⊆ {∅} → DECID ∅ ∈ 𝑦)))
46	45	alrimdv 1900	. . 3 ⊢ (𝐵 ∈ 𝑉 → (∀𝑥(𝑥 ⊆ {𝐵} → (𝑥 = ∅ ∨ 𝑥 = {𝐵})) → ∀𝑦(𝑦 ⊆ {∅} → DECID ∅ ∈ 𝑦)))
47		df-exmid 4250	. . 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 710  DECID wdc 836  ∀wal 1371   = wceq 1373  ∃wex 1516   ∈ wcel 2177  ∀wral 2485  {crab 2489  Vcvv 2773   ⊆ wss 3170  ∅c0 3464  {csn 3638  EXMIDwem 4249

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-14 2180  ax-ext 2188  ax-sep 4173  ax-nul 4181  ax-pow 4229

This theorem depends on definitions:  df-bi 117  df-dc 837  df-tru 1376  df-fal 1379  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-ne 2378  df-ral 2490  df-rab 2494  df-v 2775  df-dif 3172  df-in 3176  df-ss 3183  df-nul 3465  df-pw 3623  df-sn 3644  df-exmid 4250

This theorem is referenced by:  exmidunben  12882