Theorem onsucelsucexmid 4197

Description: The converse of onsucelsucr 4181 implies excluded middle. On the other hand, if y is constrained to be a natural number, instead of an arbitrary ordinal, then the converse of onsucelsucr 4181 does hold, as seen at nnsucelsuc 5983. (Contributed by Jim Kingdon, 2-Aug-2019.)

Hypothesis

Ref	Expression
onsucelsucexmid.1	⊢ ∀x ∈ On ∀y ∈ On (x ∈ y → suc x ∈ suc y)

Assertion

Ref	Expression
onsucelsucexmid	⊢ (φ ∨ ¬ φ)

Distinct variable group:   φ,x,y

Proof of Theorem onsucelsucexmid

Dummy variable z is distinct from all other variables.

Step	Hyp	Ref	Expression
1		onsucelsucexmidlem1 4195	. . . 4 ⊢ ∅ ∈ {z ∈ {∅, {∅}} ∣ (z = ∅ ∨ φ)}
2		0elon 4076	. . . . . 6 ⊢ ∅ ∈ On
3		onsucelsucexmidlem 4196	. . . . . 6 ⊢ {z ∈ {∅, {∅}} ∣ (z = ∅ ∨ φ)} ∈ On
4	2, 3	pm3.2i 257	. . . . 5 ⊢ (∅ ∈ On ∧ {z ∈ {∅, {∅}} ∣ (z = ∅ ∨ φ)} ∈ On)
5		onsucelsucexmid.1	. . . . 5 ⊢ ∀x ∈ On ∀y ∈ On (x ∈ y → suc x ∈ suc y)
6		eleq1 2082	. . . . . . 7 ⊢ (x = ∅ → (x ∈ y ↔ ∅ ∈ y))
7		suceq 4086	. . . . . . . 8 ⊢ (x = ∅ → suc x = suc ∅)
8	7	eleq1d 2088	. . . . . . 7 ⊢ (x = ∅ → (suc x ∈ suc y ↔ suc ∅ ∈ suc y))
9	6, 8	imbi12d 223	. . . . . 6 ⊢ (x = ∅ → ((x ∈ y → suc x ∈ suc y) ↔ (∅ ∈ y → suc ∅ ∈ suc y)))
10		eleq2 2083	. . . . . . 7 ⊢ (y = {z ∈ {∅, {∅}} ∣ (z = ∅ ∨ φ)} → (∅ ∈ y ↔ ∅ ∈ {z ∈ {∅, {∅}} ∣ (z = ∅ ∨ φ)}))
11		suceq 4086	. . . . . . . 8 ⊢ (y = {z ∈ {∅, {∅}} ∣ (z = ∅ ∨ φ)} → suc y = suc {z ∈ {∅, {∅}} ∣ (z = ∅ ∨ φ)})
12	11	eleq2d 2089	. . . . . . 7 ⊢ (y = {z ∈ {∅, {∅}} ∣ (z = ∅ ∨ φ)} → (suc ∅ ∈ suc y ↔ suc ∅ ∈ suc {z ∈ {∅, {∅}} ∣ (z = ∅ ∨ φ)}))
13	10, 12	imbi12d 223	. . . . . 6 ⊢ (y = {z ∈ {∅, {∅}} ∣ (z = ∅ ∨ φ)} → ((∅ ∈ y → suc ∅ ∈ suc y) ↔ (∅ ∈ {z ∈ {∅, {∅}} ∣ (z = ∅ ∨ φ)} → suc ∅ ∈ suc {z ∈ {∅, {∅}} ∣ (z = ∅ ∨ φ)})))
14	9, 13	rspc2va 2638	. . . . 5 ⊢ (((∅ ∈ On ∧ {z ∈ {∅, {∅}} ∣ (z = ∅ ∨ φ)} ∈ On) ∧ ∀x ∈ On ∀y ∈ On (x ∈ y → suc x ∈ suc y)) → (∅ ∈ {z ∈ {∅, {∅}} ∣ (z = ∅ ∨ φ)} → suc ∅ ∈ suc {z ∈ {∅, {∅}} ∣ (z = ∅ ∨ φ)}))
15	4, 5, 14	mp2an 404	. . . 4 ⊢ (∅ ∈ {z ∈ {∅, {∅}} ∣ (z = ∅ ∨ φ)} → suc ∅ ∈ suc {z ∈ {∅, {∅}} ∣ (z = ∅ ∨ φ)})
16	1, 15	ax-mp 7	. . 3 ⊢ suc ∅ ∈ suc {z ∈ {∅, {∅}} ∣ (z = ∅ ∨ φ)}
17		elsuci 4087	. . 3 ⊢ (suc ∅ ∈ suc {z ∈ {∅, {∅}} ∣ (z = ∅ ∨ φ)} → (suc ∅ ∈ {z ∈ {∅, {∅}} ∣ (z = ∅ ∨ φ)} ∨ suc ∅ = {z ∈ {∅, {∅}} ∣ (z = ∅ ∨ φ)}))
18	16, 17	ax-mp 7	. 2 ⊢ (suc ∅ ∈ {z ∈ {∅, {∅}} ∣ (z = ∅ ∨ φ)} ∨ suc ∅ = {z ∈ {∅, {∅}} ∣ (z = ∅ ∨ φ)})
19		suc0 4095	. . . . . 6 ⊢ suc ∅ = {∅}
20		p0ex 3911	. . . . . . 7 ⊢ {∅} ∈ V
21	20	prid2 3449	. . . . . 6 ⊢ {∅} ∈ {∅, {∅}}
22	19, 21	eqeltri 2092	. . . . 5 ⊢ suc ∅ ∈ {∅, {∅}}
23		eqeq1 2028	. . . . . . 7 ⊢ (z = suc ∅ → (z = ∅ ↔ suc ∅ = ∅))
24	23	orbi1d 692	. . . . . 6 ⊢ (z = suc ∅ → ((z = ∅ ∨ φ) ↔ (suc ∅ = ∅ ∨ φ)))
25	24	elrab3 2674	. . . . 5 ⊢ (suc ∅ ∈ {∅, {∅}} → (suc ∅ ∈ {z ∈ {∅, {∅}} ∣ (z = ∅ ∨ φ)} ↔ (suc ∅ = ∅ ∨ φ)))
26	22, 25	ax-mp 7	. . . 4 ⊢ (suc ∅ ∈ {z ∈ {∅, {∅}} ∣ (z = ∅ ∨ φ)} ↔ (suc ∅ = ∅ ∨ φ))
27		0ex 3856	. . . . . . 7 ⊢ ∅ ∈ V
28		nsuceq0g 4102	. . . . . . 7 ⊢ (∅ ∈ V → suc ∅ ≠ ∅)
29	27, 28	ax-mp 7	. . . . . 6 ⊢ suc ∅ ≠ ∅
30		df-ne 2188	. . . . . 6 ⊢ (suc ∅ ≠ ∅ ↔ ¬ suc ∅ = ∅)
31	29, 30	mpbi 133	. . . . 5 ⊢ ¬ suc ∅ = ∅
32		pm2.53 628	. . . . 5 ⊢ ((suc ∅ = ∅ ∨ φ) → (¬ suc ∅ = ∅ → φ))
33	31, 32	mpi 15	. . . 4 ⊢ ((suc ∅ = ∅ ∨ φ) → φ)
34	26, 33	sylbi 114	. . 3 ⊢ (suc ∅ ∈ {z ∈ {∅, {∅}} ∣ (z = ∅ ∨ φ)} → φ)
35	19	eqeq1i 2029	. . . . 5 ⊢ (suc ∅ = {z ∈ {∅, {∅}} ∣ (z = ∅ ∨ φ)} ↔ {∅} = {z ∈ {∅, {∅}} ∣ (z = ∅ ∨ φ)})
36	19	eqeq1i 2029	. . . . . . . 8 ⊢ (suc ∅ = ∅ ↔ {∅} = ∅)
37	31, 36	mtbi 582	. . . . . . 7 ⊢ ¬ {∅} = ∅
38	20	elsnc 3371	. . . . . . 7 ⊢ ({∅} ∈ {∅} ↔ {∅} = ∅)
39	37, 38	mtbir 583	. . . . . 6 ⊢ ¬ {∅} ∈ {∅}
40		eleq2 2083	. . . . . 6 ⊢ ({∅} = {z ∈ {∅, {∅}} ∣ (z = ∅ ∨ φ)} → ({∅} ∈ {∅} ↔ {∅} ∈ {z ∈ {∅, {∅}} ∣ (z = ∅ ∨ φ)}))
41	39, 40	mtbii 586	. . . . 5 ⊢ ({∅} = {z ∈ {∅, {∅}} ∣ (z = ∅ ∨ φ)} → ¬ {∅} ∈ {z ∈ {∅, {∅}} ∣ (z = ∅ ∨ φ)})
42	35, 41	sylbi 114	. . . 4 ⊢ (suc ∅ = {z ∈ {∅, {∅}} ∣ (z = ∅ ∨ φ)} → ¬ {∅} ∈ {z ∈ {∅, {∅}} ∣ (z = ∅ ∨ φ)})
43		olc 619	. . . . 5 ⊢ (φ → ({∅} = ∅ ∨ φ))
44		eqeq1 2028	. . . . . . . 8 ⊢ (z = {∅} → (z = ∅ ↔ {∅} = ∅))
45	44	orbi1d 692	. . . . . . 7 ⊢ (z = {∅} → ((z = ∅ ∨ φ) ↔ ({∅} = ∅ ∨ φ)))
46	45	elrab3 2674	. . . . . 6 ⊢ ({∅} ∈ {∅, {∅}} → ({∅} ∈ {z ∈ {∅, {∅}} ∣ (z = ∅ ∨ φ)} ↔ ({∅} = ∅ ∨ φ)))
47	21, 46	ax-mp 7	. . . . 5 ⊢ ({∅} ∈ {z ∈ {∅, {∅}} ∣ (z = ∅ ∨ φ)} ↔ ({∅} = ∅ ∨ φ))
48	43, 47	sylibr 137	. . . 4 ⊢ (φ → {∅} ∈ {z ∈ {∅, {∅}} ∣ (z = ∅ ∨ φ)})
49	42, 48	nsyl 546	. . 3 ⊢ (suc ∅ = {z ∈ {∅, {∅}} ∣ (z = ∅ ∨ φ)} → ¬ φ)
50	34, 49	orim12i 663	. 2 ⊢ ((suc ∅ ∈ {z ∈ {∅, {∅}} ∣ (z = ∅ ∨ φ)} ∨ suc ∅ = {z ∈ {∅, {∅}} ∣ (z = ∅ ∨ φ)}) → (φ ∨ ¬ φ))
51	18, 50	ax-mp 7	1 ⊢ (φ ∨ ¬ φ)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 97   ↔ wb 98   ∨ wo 616   = wceq 1228   ∈ wcel 1374   ≠ wne 2186  ∀wral 2282  {crab 2286  Vcvv 2533  ∅c0 3199  {csn 3348  {cpr 3349  Oncon0 4047  suc csuc 4049

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 532  ax-in2 533  ax-io 617  ax-5 1316  ax-7 1317  ax-gen 1318  ax-ie1 1363  ax-ie2 1364  ax-8 1376  ax-10 1377  ax-11 1378  ax-i12 1379  ax-bnd 1380  ax-4 1381  ax-14 1386  ax-17 1400  ax-i9 1404  ax-ial 1409  ax-i5r 1410  ax-ext 2004  ax-sep 3847  ax-nul 3855  ax-pow 3899

This theorem depends on definitions:  df-bi 110  df-3an 875  df-tru 1231  df-nf 1330  df-sb 1628  df-clab 2009  df-cleq 2015  df-clel 2018  df-nfc 2149  df-ne 2188  df-ral 2287  df-rex 2288  df-rab 2291  df-v 2535  df-dif 2895  df-un 2897  df-in 2899  df-ss 2906  df-nul 3200  df-pw 3334  df-sn 3354  df-pr 3355  df-uni 3553  df-tr 3827  df-iord 4050  df-on 4052  df-suc 4055

This theorem is referenced by:  ordsucunielexmid  4198