Theorem exmidsssnc 4286

Description: Excluded middle in terms of subsets of a singleton. This is similar to exmid01 4281 but lets you choose any set as the element of the singleton rather than just ∅. It is similar to exmidsssn 4285 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 4285	. . . 4 ⊢ (EXMID ↔ ∀𝑥∀𝑢(𝑥 ⊆ {𝑢} ↔ (𝑥 = ∅ ∨ 𝑥 = {𝑢})))
2		sneq 3677	. . . . . . . 8 ⊢ (𝑢 = 𝐵 → {𝑢} = {𝐵})
3	2	sseq2d 3254	. . . . . . 7 ⊢ (𝑢 = 𝐵 → (𝑥 ⊆ {𝑢} ↔ 𝑥 ⊆ {𝐵}))
4	2	eqeq2d 2241	. . . . . . . 8 ⊢ (𝑢 = 𝐵 → (𝑥 = {𝑢} ↔ 𝑥 = {𝐵}))
5	4	orbi2d 795	. . . . . . 7 ⊢ (𝑢 = 𝐵 → ((𝑥 = ∅ ∨ 𝑥 = {𝑢}) ↔ (𝑥 = ∅ ∨ 𝑥 = {𝐵})))
6	3, 5	bibi12d 235	. . . . . 6 ⊢ (𝑢 = 𝐵 → ((𝑥 ⊆ {𝑢} ↔ (𝑥 = ∅ ∨ 𝑥 = {𝑢})) ↔ (𝑥 ⊆ {𝐵} ↔ (𝑥 = ∅ ∨ 𝑥 = {𝐵}))))
7	6	spcgv 2890	. . . . 5 ⊢ (𝐵 ∈ 𝑉 → (∀𝑢(𝑥 ⊆ {𝑢} ↔ (𝑥 = ∅ ∨ 𝑥 = {𝑢})) → (𝑥 ⊆ {𝐵} ↔ (𝑥 = ∅ ∨ 𝑥 = {𝐵}))))
8	7	alimdv 1925	. . . 4 ⊢ (𝐵 ∈ 𝑉 → (∀𝑥∀𝑢(𝑥 ⊆ {𝑢} ↔ (𝑥 = ∅ ∨ 𝑥 = {𝑢})) → ∀𝑥(𝑥 ⊆ {𝐵} ↔ (𝑥 = ∅ ∨ 𝑥 = {𝐵}))))
9	1, 8	biimtrid 152	. . 3 ⊢ (𝐵 ∈ 𝑉 → (EXMID → ∀𝑥(𝑥 ⊆ {𝐵} ↔ (𝑥 = ∅ ∨ 𝑥 = {𝐵}))))
10		biimp 118	. . . 4 ⊢ ((𝑥 ⊆ {𝐵} ↔ (𝑥 = ∅ ∨ 𝑥 = {𝐵})) → (𝑥 ⊆ {𝐵} → (𝑥 = ∅ ∨ 𝑥 = {𝐵})))
11	10	alimi 1501	. . 3 ⊢ (∀𝑥(𝑥 ⊆ {𝐵} ↔ (𝑥 = ∅ ∨ 𝑥 = {𝐵})) → ∀𝑥(𝑥 ⊆ {𝐵} → (𝑥 = ∅ ∨ 𝑥 = {𝐵})))
12	9, 11	syl6 33	. 2 ⊢ (𝐵 ∈ 𝑉 → (EXMID → ∀𝑥(𝑥 ⊆ {𝐵} → (𝑥 = ∅ ∨ 𝑥 = {𝐵}))))
13		ssrab2 3309	. . . . . . . . 9 ⊢ {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} ⊆ {𝐵}
14		snexg 4267	. . . . . . . . . 10 ⊢ (𝐵 ∈ 𝑉 → {𝐵} ∈ V)
15		rabexg 4226	. . . . . . . . . 10 ⊢ ({𝐵} ∈ V → {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} ∈ V)
16		sseq1 3247	. . . . . . . . . . . 12 ⊢ (𝑥 = {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} → (𝑥 ⊆ {𝐵} ↔ {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} ⊆ {𝐵}))
17		eqeq1 2236	. . . . . . . . . . . . 13 ⊢ (𝑥 = {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} → (𝑥 = ∅ ↔ {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = ∅))
18		eqeq1 2236	. . . . . . . . . . . . 13 ⊢ (𝑥 = {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} → (𝑥 = {𝐵} ↔ {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = {𝐵}))
19	17, 18	orbi12d 798	. . . . . . . . . . . 12 ⊢ (𝑥 = {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} → ((𝑥 = ∅ ∨ 𝑥 = {𝐵}) ↔ ({𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = ∅ ∨ {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = {𝐵})))
20	16, 19	imbi12d 234	. . . . . . . . . . 11 ⊢ (𝑥 = {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} → ((𝑥 ⊆ {𝐵} → (𝑥 = ∅ ∨ 𝑥 = {𝐵})) ↔ ({𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} ⊆ {𝐵} → ({𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = ∅ ∨ {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = {𝐵}))))
21	20	spcgv 2890	. . . . . . . . . 10 ⊢ ({𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} ∈ V → (∀𝑥(𝑥 ⊆ {𝐵} → (𝑥 = ∅ ∨ 𝑥 = {𝐵})) → ({𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} ⊆ {𝐵} → ({𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = ∅ ∨ {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = {𝐵}))))
22	14, 15, 21	3syl 17	. . . . . . . . 9 ⊢ (𝐵 ∈ 𝑉 → (∀𝑥(𝑥 ⊆ {𝐵} → (𝑥 = ∅ ∨ 𝑥 = {𝐵})) → ({𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} ⊆ {𝐵} → ({𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = ∅ ∨ {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = {𝐵}))))
23	13, 22	mpii 44	. . . . . . . 8 ⊢ (𝐵 ∈ 𝑉 → (∀𝑥(𝑥 ⊆ {𝐵} → (𝑥 = ∅ ∨ 𝑥 = {𝐵})) → ({𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = ∅ ∨ {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = {𝐵})))
24		rabeq0 3521	. . . . . . . . . . 11 ⊢ ({𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = ∅ ↔ ∀𝑧 ∈ {𝐵} ¬ ∅ ∈ 𝑦)
25		snmg 3784	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ 𝑉 → ∃𝑤 𝑤 ∈ {𝐵})
26		r19.3rmv 3582	. . . . . . . . . . . 12 ⊢ (∃𝑤 𝑤 ∈ {𝐵} → (¬ ∅ ∈ 𝑦 ↔ ∀𝑧 ∈ {𝐵} ¬ ∅ ∈ 𝑦))
27	25, 26	syl 14	. . . . . . . . . . 11 ⊢ (𝐵 ∈ 𝑉 → (¬ ∅ ∈ 𝑦 ↔ ∀𝑧 ∈ {𝐵} ¬ ∅ ∈ 𝑦))
28	24, 27	bitr4id 199	. . . . . . . . . 10 ⊢ (𝐵 ∈ 𝑉 → ({𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = ∅ ↔ ¬ ∅ ∈ 𝑦))
29	28	biimpd 144	. . . . . . . . 9 ⊢ (𝐵 ∈ 𝑉 → ({𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = ∅ → ¬ ∅ ∈ 𝑦))
30		snidg 3695	. . . . . . . . . . . . 13 ⊢ (𝐵 ∈ 𝑉 → 𝐵 ∈ {𝐵})
31	30	adantr 276	. . . . . . . . . . . 12 ⊢ ((𝐵 ∈ 𝑉 ∧ {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = {𝐵}) → 𝐵 ∈ {𝐵})
32		simpr 110	. . . . . . . . . . . 12 ⊢ ((𝐵 ∈ 𝑉 ∧ {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = {𝐵}) → {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = {𝐵})
33	31, 32	eleqtrrd 2309	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ 𝑉 ∧ {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = {𝐵}) → 𝐵 ∈ {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦})
34		biidd 172	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝐵 → (∅ ∈ 𝑦 ↔ ∅ ∈ 𝑦))
35	34	elrab 2959	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} ↔ (𝐵 ∈ {𝐵} ∧ ∅ ∈ 𝑦))
36	35	simprbi 275	. . . . . . . . . . 11 ⊢ (𝐵 ∈ {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} → ∅ ∈ 𝑦)
37	33, 36	syl 14	. . . . . . . . . 10 ⊢ ((𝐵 ∈ 𝑉 ∧ {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = {𝐵}) → ∅ ∈ 𝑦)
38	37	ex 115	. . . . . . . . 9 ⊢ (𝐵 ∈ 𝑉 → ({𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = {𝐵} → ∅ ∈ 𝑦))
39	29, 38	orim12d 791	. . . . . . . 8 ⊢ (𝐵 ∈ 𝑉 → (({𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = ∅ ∨ {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = {𝐵}) → (¬ ∅ ∈ 𝑦 ∨ ∅ ∈ 𝑦)))
40	23, 39	syld 45	. . . . . . 7 ⊢ (𝐵 ∈ 𝑉 → (∀𝑥(𝑥 ⊆ {𝐵} → (𝑥 = ∅ ∨ 𝑥 = {𝐵})) → (¬ ∅ ∈ 𝑦 ∨ ∅ ∈ 𝑦)))
41		orcom 733	. . . . . . 7 ⊢ ((¬ ∅ ∈ 𝑦 ∨ ∅ ∈ 𝑦) ↔ (∅ ∈ 𝑦 ∨ ¬ ∅ ∈ 𝑦))
42	40, 41	imbitrdi 161	. . . . . 6 ⊢ (𝐵 ∈ 𝑉 → (∀𝑥(𝑥 ⊆ {𝐵} → (𝑥 = ∅ ∨ 𝑥 = {𝐵})) → (∅ ∈ 𝑦 ∨ ¬ ∅ ∈ 𝑦)))
43		df-dc 840	. . . . . 6 ⊢ (DECID ∅ ∈ 𝑦 ↔ (∅ ∈ 𝑦 ∨ ¬ ∅ ∈ 𝑦))
44	42, 43	imbitrrdi 162	. . . . 5 ⊢ (𝐵 ∈ 𝑉 → (∀𝑥(𝑥 ⊆ {𝐵} → (𝑥 = ∅ ∨ 𝑥 = {𝐵})) → DECID ∅ ∈ 𝑦))
45	44	a1dd 48	. . . 4 ⊢ (𝐵 ∈ 𝑉 → (∀𝑥(𝑥 ⊆ {𝐵} → (𝑥 = ∅ ∨ 𝑥 = {𝐵})) → (𝑦 ⊆ {∅} → DECID ∅ ∈ 𝑦)))
46	45	alrimdv 1922	. . 3 ⊢ (𝐵 ∈ 𝑉 → (∀𝑥(𝑥 ⊆ {𝐵} → (𝑥 = ∅ ∨ 𝑥 = {𝐵})) → ∀𝑦(𝑦 ⊆ {∅} → DECID ∅ ∈ 𝑦)))
47		df-exmid 4278	. . 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 713  DECID wdc 839  ∀wal 1393   = wceq 1395  ∃wex 1538   ∈ wcel 2200  ∀wral 2508  {crab 2512  Vcvv 2799   ⊆ wss 3197  ∅c0 3491  {csn 3666  EXMIDwem 4277

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 617  ax-in2 618  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-14 2203  ax-ext 2211  ax-sep 4201  ax-nul 4209  ax-pow 4257

This theorem depends on definitions:  df-bi 117  df-dc 840  df-tru 1398  df-fal 1401  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ne 2401  df-ral 2513  df-rab 2517  df-v 2801  df-dif 3199  df-in 3203  df-ss 3210  df-nul 3492  df-pw 3651  df-sn 3672  df-exmid 4278

This theorem is referenced by:  exmidunben  12992