Theorem undifexmid 4256

Description: Union of complementary parts producing the whole and excluded middle. Although special cases such as undifss 3552 and undifdcss 7053 are provable, the full statement implies excluded middle as shown here. (Contributed by Jim Kingdon, 16-Jun-2022.)

Hypothesis

Ref	Expression
undifexmid.1	⊢ (𝑥 ⊆ 𝑦 ↔ (𝑥 ∪ (𝑦 ∖ 𝑥)) = 𝑦)

Assertion

Ref	Expression
undifexmid	⊢ (𝜑 ∨ ¬ 𝜑)

Distinct variable group:   𝜑,𝑥,𝑦

Proof of Theorem undifexmid

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		0ex 4190	. . . . 5 ⊢ ∅ ∈ V
2	1	snid 3677	. . . 4 ⊢ ∅ ∈ {∅}
3		ssrab2 3289	. . . . 5 ⊢ {𝑧 ∈ {∅} ∣ 𝜑} ⊆ {∅}
4		p0ex 4251	. . . . . . 7 ⊢ {∅} ∈ V
5	4	rabex 4207	. . . . . 6 ⊢ {𝑧 ∈ {∅} ∣ 𝜑} ∈ V
6		sseq12 3229	. . . . . . 7 ⊢ ((𝑥 = {𝑧 ∈ {∅} ∣ 𝜑} ∧ 𝑦 = {∅}) → (𝑥 ⊆ 𝑦 ↔ {𝑧 ∈ {∅} ∣ 𝜑} ⊆ {∅}))
7		simpl 109	. . . . . . . . 9 ⊢ ((𝑥 = {𝑧 ∈ {∅} ∣ 𝜑} ∧ 𝑦 = {∅}) → 𝑥 = {𝑧 ∈ {∅} ∣ 𝜑})
8		simpr 110	. . . . . . . . . 10 ⊢ ((𝑥 = {𝑧 ∈ {∅} ∣ 𝜑} ∧ 𝑦 = {∅}) → 𝑦 = {∅})
9	8, 7	difeq12d 3303	. . . . . . . . 9 ⊢ ((𝑥 = {𝑧 ∈ {∅} ∣ 𝜑} ∧ 𝑦 = {∅}) → (𝑦 ∖ 𝑥) = ({∅} ∖ {𝑧 ∈ {∅} ∣ 𝜑}))
10	7, 9	uneq12d 3339	. . . . . . . 8 ⊢ ((𝑥 = {𝑧 ∈ {∅} ∣ 𝜑} ∧ 𝑦 = {∅}) → (𝑥 ∪ (𝑦 ∖ 𝑥)) = ({𝑧 ∈ {∅} ∣ 𝜑} ∪ ({∅} ∖ {𝑧 ∈ {∅} ∣ 𝜑})))
11	10, 8	eqeq12d 2224	. . . . . . 7 ⊢ ((𝑥 = {𝑧 ∈ {∅} ∣ 𝜑} ∧ 𝑦 = {∅}) → ((𝑥 ∪ (𝑦 ∖ 𝑥)) = 𝑦 ↔ ({𝑧 ∈ {∅} ∣ 𝜑} ∪ ({∅} ∖ {𝑧 ∈ {∅} ∣ 𝜑})) = {∅}))
12	6, 11	bibi12d 235	. . . . . 6 ⊢ ((𝑥 = {𝑧 ∈ {∅} ∣ 𝜑} ∧ 𝑦 = {∅}) → ((𝑥 ⊆ 𝑦 ↔ (𝑥 ∪ (𝑦 ∖ 𝑥)) = 𝑦) ↔ ({𝑧 ∈ {∅} ∣ 𝜑} ⊆ {∅} ↔ ({𝑧 ∈ {∅} ∣ 𝜑} ∪ ({∅} ∖ {𝑧 ∈ {∅} ∣ 𝜑})) = {∅})))
13		undifexmid.1	. . . . . 6 ⊢ (𝑥 ⊆ 𝑦 ↔ (𝑥 ∪ (𝑦 ∖ 𝑥)) = 𝑦)
14	5, 4, 12, 13	vtocl2 2836	. . . . 5 ⊢ ({𝑧 ∈ {∅} ∣ 𝜑} ⊆ {∅} ↔ ({𝑧 ∈ {∅} ∣ 𝜑} ∪ ({∅} ∖ {𝑧 ∈ {∅} ∣ 𝜑})) = {∅})
15	3, 14	mpbi 145	. . . 4 ⊢ ({𝑧 ∈ {∅} ∣ 𝜑} ∪ ({∅} ∖ {𝑧 ∈ {∅} ∣ 𝜑})) = {∅}
16	2, 15	eleqtrri 2285	. . 3 ⊢ ∅ ∈ ({𝑧 ∈ {∅} ∣ 𝜑} ∪ ({∅} ∖ {𝑧 ∈ {∅} ∣ 𝜑}))
17		elun 3325	. . 3 ⊢ (∅ ∈ ({𝑧 ∈ {∅} ∣ 𝜑} ∪ ({∅} ∖ {𝑧 ∈ {∅} ∣ 𝜑})) ↔ (∅ ∈ {𝑧 ∈ {∅} ∣ 𝜑} ∨ ∅ ∈ ({∅} ∖ {𝑧 ∈ {∅} ∣ 𝜑})))
18	16, 17	mpbi 145	. 2 ⊢ (∅ ∈ {𝑧 ∈ {∅} ∣ 𝜑} ∨ ∅ ∈ ({∅} ∖ {𝑧 ∈ {∅} ∣ 𝜑}))
19		biidd 172	. . . . . 6 ⊢ (𝑧 = ∅ → (𝜑 ↔ 𝜑))
20	19	elrab3 2940	. . . . 5 ⊢ (∅ ∈ {∅} → (∅ ∈ {𝑧 ∈ {∅} ∣ 𝜑} ↔ 𝜑))
21	2, 20	ax-mp 5	. . . 4 ⊢ (∅ ∈ {𝑧 ∈ {∅} ∣ 𝜑} ↔ 𝜑)
22	21	biimpi 120	. . 3 ⊢ (∅ ∈ {𝑧 ∈ {∅} ∣ 𝜑} → 𝜑)
23		eldifn 3307	. . . 4 ⊢ (∅ ∈ ({∅} ∖ {𝑧 ∈ {∅} ∣ 𝜑}) → ¬ ∅ ∈ {𝑧 ∈ {∅} ∣ 𝜑})
24	23, 21	sylnib 680	. . 3 ⊢ (∅ ∈ ({∅} ∖ {𝑧 ∈ {∅} ∣ 𝜑}) → ¬ 𝜑)
25	22, 24	orim12i 763	. 2 ⊢ ((∅ ∈ {𝑧 ∈ {∅} ∣ 𝜑} ∨ ∅ ∈ ({∅} ∖ {𝑧 ∈ {∅} ∣ 𝜑})) → (𝜑 ∨ ¬ 𝜑))
26	18, 25	ax-mp 5	1 ⊢ (𝜑 ∨ ¬ 𝜑)

Syntax hints:  ¬ wn 3   ∧ wa 104   ↔ wb 105   ∨ wo 712   = wceq 1375   ∈ wcel 2180  {crab 2492   ∖ cdif 3174   ∪ cun 3175   ⊆ wss 3177  ∅c0 3471  {csn 3646

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 713  ax-5 1473  ax-7 1474  ax-gen 1475  ax-ie1 1519  ax-ie2 1520  ax-8 1530  ax-10 1531  ax-11 1532  ax-i12 1533  ax-bndl 1535  ax-4 1536  ax-17 1552  ax-i9 1556  ax-ial 1560  ax-i5r 1561  ax-14 2183  ax-ext 2191  ax-sep 4181  ax-nul 4189  ax-pow 4237

This theorem depends on definitions:  df-bi 117  df-tru 1378  df-nf 1487  df-sb 1789  df-clab 2196  df-cleq 2202  df-clel 2205  df-nfc 2341  df-ral 2493  df-rab 2497  df-v 2781  df-dif 3179  df-un 3181  df-in 3183  df-ss 3190  df-nul 3472  df-pw 3631  df-sn 3652

This theorem is referenced by: (None)