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 5980. (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 2083	. . . . . . 7 ⊢ (x = ∅ → (x ∈ y ↔ ∅ ∈ y))
7		suceq 4086	. . . . . . . 8 ⊢ (x = ∅ → suc x = suc ∅)
8	7	eleq1d 2089	. . . . . . 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 2084	. . . . . . 7 ⊢ (y = {z ∈ {∅, {∅}} ∣ (z = ∅ ∨ φ)} → (∅ ∈ y ↔ ∅ ∈ {z ∈ {∅, {∅}} ∣ (z = ∅ ∨ φ)}))
11		suceq 4086	. . . . . . . 8 ⊢ (y = {z ∈ {∅, {∅}} ∣ (z = ∅ ∨ φ)} → suc y = suc {z ∈ {∅, {∅}} ∣ (z = ∅ ∨ φ)})
12	11	eleq2d 2090	. . . . . . 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 2639	. . . . 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 3912	. . . . . . 7 ⊢ {∅} ∈ V
21	20	prid2 3450	. . . . . 6 ⊢ {∅} ∈ {∅, {∅}}
22	19, 21	eqeltri 2093	. . . . 5 ⊢ suc ∅ ∈ {∅, {∅}}
23		eqeq1 2029	. . . . . . 7 ⊢ (z = suc ∅ → (z = ∅ ↔ suc ∅ = ∅))
24	23	orbi1d 692	. . . . . 6 ⊢ (z = suc ∅ → ((z = ∅ ∨ φ) ↔ (suc ∅ = ∅ ∨ φ)))
25	24	elrab3 2675	. . . . 5 ⊢ (suc ∅ ∈ {∅, {∅}} → (suc ∅ ∈ {z ∈ {∅, {∅}} ∣ (z = ∅ ∨ φ)} ↔ (suc ∅ = ∅ ∨ φ)))
26	22, 25	ax-mp 7	. . . 4 ⊢ (suc ∅ ∈ {z ∈ {∅, {∅}} ∣ (z = ∅ ∨ φ)} ↔ (suc ∅ = ∅ ∨ φ))
27		0ex 3857	. . . . . . 7 ⊢ ∅ ∈ V
28		nsuceq0g 4102	. . . . . . 7 ⊢ (∅ ∈ V → suc ∅ ≠ ∅)
29	27, 28	ax-mp 7	. . . . . 6 ⊢ suc ∅ ≠ ∅
30		df-ne 2189	. . . . . 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 2030	. . . . 5 ⊢ (suc ∅ = {z ∈ {∅, {∅}} ∣ (z = ∅ ∨ φ)} ↔ {∅} = {z ∈ {∅, {∅}} ∣ (z = ∅ ∨ φ)})
36	19	eqeq1i 2030	. . . . . . . 8 ⊢ (suc ∅ = ∅ ↔ {∅} = ∅)
37	31, 36	mtbi 582	. . . . . . 7 ⊢ ¬ {∅} = ∅
38	20	elsnc 3372	. . . . . . 7 ⊢ ({∅} ∈ {∅} ↔ {∅} = ∅)
39	37, 38	mtbir 583	. . . . . 6 ⊢ ¬ {∅} ∈ {∅}
40		eleq2 2084	. . . . . 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 2029	. . . . . . . 8 ⊢ (z = {∅} → (z = ∅ ↔ {∅} = ∅))
45	44	orbi1d 692	. . . . . . 7 ⊢ (z = {∅} → ((z = ∅ ∨ φ) ↔ ({∅} = ∅ ∨ φ)))
46	45	elrab3 2675	. . . . . 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 1375   ≠ wne 2187  ∀wral 2283  {crab 2287  Vcvv 2534  ∅c0 3200  {csn 3349  {cpr 3350  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 1364  ax-ie2 1365  ax-8 1377  ax-10 1378  ax-11 1379  ax-i12 1380  ax-bnd 1381  ax-4 1382  ax-14 1387  ax-17 1401  ax-i9 1405  ax-ial 1410  ax-i5r 1411  ax-ext 2005  ax-sep 3848  ax-nul 3856  ax-pow 3900

This theorem depends on definitions:  df-bi 110  df-3an 875  df-tru 1231  df-nf 1330  df-sb 1629  df-clab 2010  df-cleq 2016  df-clel 2019  df-nfc 2150  df-ne 2189  df-ral 2288  df-rex 2289  df-rab 2292  df-v 2536  df-dif 2896  df-un 2898  df-in 2900  df-ss 2907  df-nul 3201  df-pw 3335  df-sn 3355  df-pr 3356  df-uni 3554  df-tr 3828  df-iord 4050  df-on 4052  df-suc 4055

This theorem is referenced by:  ordsucunielexmid  4198