Theorem exmidsssnc 4236

Description: Excluded middle in terms of subsets of a singleton. This is similar to exmid01 4231 but lets you choose any set as the element of the singleton rather than just ∅. It is similar to exmidsssn 4235 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 4235	. . . 4 ⊢ (EXMID ↔ ∀𝑥∀𝑢(𝑥 ⊆ {𝑢} ↔ (𝑥 = ∅ ∨ 𝑥 = {𝑢})))
2		sneq 3633	. . . . . . . 8 ⊢ (𝑢 = 𝐵 → {𝑢} = {𝐵})
3	2	sseq2d 3213	. . . . . . 7 ⊢ (𝑢 = 𝐵 → (𝑥 ⊆ {𝑢} ↔ 𝑥 ⊆ {𝐵}))
4	2	eqeq2d 2208	. . . . . . . 8 ⊢ (𝑢 = 𝐵 → (𝑥 = {𝑢} ↔ 𝑥 = {𝐵}))
5	4	orbi2d 791	. . . . . . 7 ⊢ (𝑢 = 𝐵 → ((𝑥 = ∅ ∨ 𝑥 = {𝑢}) ↔ (𝑥 = ∅ ∨ 𝑥 = {𝐵})))
6	3, 5	bibi12d 235	. . . . . 6 ⊢ (𝑢 = 𝐵 → ((𝑥 ⊆ {𝑢} ↔ (𝑥 = ∅ ∨ 𝑥 = {𝑢})) ↔ (𝑥 ⊆ {𝐵} ↔ (𝑥 = ∅ ∨ 𝑥 = {𝐵}))))
7	6	spcgv 2851	. . . . 5 ⊢ (𝐵 ∈ 𝑉 → (∀𝑢(𝑥 ⊆ {𝑢} ↔ (𝑥 = ∅ ∨ 𝑥 = {𝑢})) → (𝑥 ⊆ {𝐵} ↔ (𝑥 = ∅ ∨ 𝑥 = {𝐵}))))
8	7	alimdv 1893	. . . 4 ⊢ (𝐵 ∈ 𝑉 → (∀𝑥∀𝑢(𝑥 ⊆ {𝑢} ↔ (𝑥 = ∅ ∨ 𝑥 = {𝑢})) → ∀𝑥(𝑥 ⊆ {𝐵} ↔ (𝑥 = ∅ ∨ 𝑥 = {𝐵}))))
9	1, 8	biimtrid 152	. . 3 ⊢ (𝐵 ∈ 𝑉 → (EXMID → ∀𝑥(𝑥 ⊆ {𝐵} ↔ (𝑥 = ∅ ∨ 𝑥 = {𝐵}))))
10		biimp 118	. . . 4 ⊢ ((𝑥 ⊆ {𝐵} ↔ (𝑥 = ∅ ∨ 𝑥 = {𝐵})) → (𝑥 ⊆ {𝐵} → (𝑥 = ∅ ∨ 𝑥 = {𝐵})))
11	10	alimi 1469	. . 3 ⊢ (∀𝑥(𝑥 ⊆ {𝐵} ↔ (𝑥 = ∅ ∨ 𝑥 = {𝐵})) → ∀𝑥(𝑥 ⊆ {𝐵} → (𝑥 = ∅ ∨ 𝑥 = {𝐵})))
12	9, 11	syl6 33	. 2 ⊢ (𝐵 ∈ 𝑉 → (EXMID → ∀𝑥(𝑥 ⊆ {𝐵} → (𝑥 = ∅ ∨ 𝑥 = {𝐵}))))
13		ssrab2 3268	. . . . . . . . 9 ⊢ {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} ⊆ {𝐵}
14		snexg 4217	. . . . . . . . . 10 ⊢ (𝐵 ∈ 𝑉 → {𝐵} ∈ V)
15		rabexg 4176	. . . . . . . . . 10 ⊢ ({𝐵} ∈ V → {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} ∈ V)
16		sseq1 3206	. . . . . . . . . . . 12 ⊢ (𝑥 = {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} → (𝑥 ⊆ {𝐵} ↔ {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} ⊆ {𝐵}))
17		eqeq1 2203	. . . . . . . . . . . . 13 ⊢ (𝑥 = {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} → (𝑥 = ∅ ↔ {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = ∅))
18		eqeq1 2203	. . . . . . . . . . . . 13 ⊢ (𝑥 = {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} → (𝑥 = {𝐵} ↔ {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = {𝐵}))
19	17, 18	orbi12d 794	. . . . . . . . . . . 12 ⊢ (𝑥 = {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} → ((𝑥 = ∅ ∨ 𝑥 = {𝐵}) ↔ ({𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = ∅ ∨ {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = {𝐵})))
20	16, 19	imbi12d 234	. . . . . . . . . . 11 ⊢ (𝑥 = {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} → ((𝑥 ⊆ {𝐵} → (𝑥 = ∅ ∨ 𝑥 = {𝐵})) ↔ ({𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} ⊆ {𝐵} → ({𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = ∅ ∨ {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = {𝐵}))))
21	20	spcgv 2851	. . . . . . . . . 10 ⊢ ({𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} ∈ V → (∀𝑥(𝑥 ⊆ {𝐵} → (𝑥 = ∅ ∨ 𝑥 = {𝐵})) → ({𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} ⊆ {𝐵} → ({𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = ∅ ∨ {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = {𝐵}))))
22	14, 15, 21	3syl 17	. . . . . . . . 9 ⊢ (𝐵 ∈ 𝑉 → (∀𝑥(𝑥 ⊆ {𝐵} → (𝑥 = ∅ ∨ 𝑥 = {𝐵})) → ({𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} ⊆ {𝐵} → ({𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = ∅ ∨ {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = {𝐵}))))
23	13, 22	mpii 44	. . . . . . . 8 ⊢ (𝐵 ∈ 𝑉 → (∀𝑥(𝑥 ⊆ {𝐵} → (𝑥 = ∅ ∨ 𝑥 = {𝐵})) → ({𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = ∅ ∨ {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = {𝐵})))
24		rabeq0 3480	. . . . . . . . . . 11 ⊢ ({𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = ∅ ↔ ∀𝑧 ∈ {𝐵} ¬ ∅ ∈ 𝑦)
25		snmg 3740	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ 𝑉 → ∃𝑤 𝑤 ∈ {𝐵})
26		r19.3rmv 3541	. . . . . . . . . . . 12 ⊢ (∃𝑤 𝑤 ∈ {𝐵} → (¬ ∅ ∈ 𝑦 ↔ ∀𝑧 ∈ {𝐵} ¬ ∅ ∈ 𝑦))
27	25, 26	syl 14	. . . . . . . . . . 11 ⊢ (𝐵 ∈ 𝑉 → (¬ ∅ ∈ 𝑦 ↔ ∀𝑧 ∈ {𝐵} ¬ ∅ ∈ 𝑦))
28	24, 27	bitr4id 199	. . . . . . . . . 10 ⊢ (𝐵 ∈ 𝑉 → ({𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = ∅ ↔ ¬ ∅ ∈ 𝑦))
29	28	biimpd 144	. . . . . . . . 9 ⊢ (𝐵 ∈ 𝑉 → ({𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = ∅ → ¬ ∅ ∈ 𝑦))
30		snidg 3651	. . . . . . . . . . . . 13 ⊢ (𝐵 ∈ 𝑉 → 𝐵 ∈ {𝐵})
31	30	adantr 276	. . . . . . . . . . . 12 ⊢ ((𝐵 ∈ 𝑉 ∧ {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = {𝐵}) → 𝐵 ∈ {𝐵})
32		simpr 110	. . . . . . . . . . . 12 ⊢ ((𝐵 ∈ 𝑉 ∧ {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = {𝐵}) → {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = {𝐵})
33	31, 32	eleqtrrd 2276	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ 𝑉 ∧ {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦} = {𝐵}) → 𝐵 ∈ {𝑧 ∈ {𝐵} ∣ ∅ ∈ 𝑦})
34		biidd 172	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝐵 → (∅ ∈ 𝑦 ↔ ∅ ∈ 𝑦))
35	34	elrab 2920	. . . . . . . . . . . 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 1890	. . 3 ⊢ (𝐵 ∈ 𝑉 → (∀𝑥(𝑥 ⊆ {𝐵} → (𝑥 = ∅ ∨ 𝑥 = {𝐵})) → ∀𝑦(𝑦 ⊆ {∅} → DECID ∅ ∈ 𝑦)))
47		df-exmid 4228	. . 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 1506   ∈ wcel 2167  ∀wral 2475  {crab 2479  Vcvv 2763   ⊆ 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-fal 1370  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-ne 2368  df-ral 2480  df-rab 2484  df-v 2765  df-dif 3159  df-in 3163  df-ss 3170  df-nul 3451  df-pw 3607  df-sn 3628  df-exmid 4228

This theorem is referenced by:  exmidunben  12643