Theorem onsucelsucexmid 4215

Description: The converse of onsucelsucr 4199 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 4199 does hold, as seen at nnsucelsuc 6009. (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 4213	. . . 4 ⊢ ∅ ∈ {z ∈ {∅, {∅}} ∣ (z = ∅ ∨ φ)}
2		0elon 4095	. . . . . 6 ⊢ ∅ ∈ On
3		onsucelsucexmidlem 4214	. . . . . 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 2097	. . . . . . 7 ⊢ (x = ∅ → (x ∈ y ↔ ∅ ∈ y))
7		suceq 4105	. . . . . . . 8 ⊢ (x = ∅ → suc x = suc ∅)
8	7	eleq1d 2103	. . . . . . 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 2098	. . . . . . 7 ⊢ (y = {z ∈ {∅, {∅}} ∣ (z = ∅ ∨ φ)} → (∅ ∈ y ↔ ∅ ∈ {z ∈ {∅, {∅}} ∣ (z = ∅ ∨ φ)}))
11		suceq 4105	. . . . . . . 8 ⊢ (y = {z ∈ {∅, {∅}} ∣ (z = ∅ ∨ φ)} → suc y = suc {z ∈ {∅, {∅}} ∣ (z = ∅ ∨ φ)})
12	11	eleq2d 2104	. . . . . . 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 2657	. . . . 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 402	. . . 4 ⊢ (∅ ∈ {z ∈ {∅, {∅}} ∣ (z = ∅ ∨ φ)} → suc ∅ ∈ suc {z ∈ {∅, {∅}} ∣ (z = ∅ ∨ φ)})
16	1, 15	ax-mp 7	. . 3 ⊢ suc ∅ ∈ suc {z ∈ {∅, {∅}} ∣ (z = ∅ ∨ φ)}
17		elsuci 4106	. . 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 4114	. . . . . 6 ⊢ suc ∅ = {∅}
20		p0ex 3930	. . . . . . 7 ⊢ {∅} ∈ V
21	20	prid2 3468	. . . . . 6 ⊢ {∅} ∈ {∅, {∅}}
22	19, 21	eqeltri 2107	. . . . 5 ⊢ suc ∅ ∈ {∅, {∅}}
23		eqeq1 2043	. . . . . . 7 ⊢ (z = suc ∅ → (z = ∅ ↔ suc ∅ = ∅))
24	23	orbi1d 704	. . . . . 6 ⊢ (z = suc ∅ → ((z = ∅ ∨ φ) ↔ (suc ∅ = ∅ ∨ φ)))
25	24	elrab3 2693	. . . . 5 ⊢ (suc ∅ ∈ {∅, {∅}} → (suc ∅ ∈ {z ∈ {∅, {∅}} ∣ (z = ∅ ∨ φ)} ↔ (suc ∅ = ∅ ∨ φ)))
26	22, 25	ax-mp 7	. . . 4 ⊢ (suc ∅ ∈ {z ∈ {∅, {∅}} ∣ (z = ∅ ∨ φ)} ↔ (suc ∅ = ∅ ∨ φ))
27		0ex 3875	. . . . . . 7 ⊢ ∅ ∈ V
28		nsuceq0g 4121	. . . . . . 7 ⊢ (∅ ∈ V → suc ∅ ≠ ∅)
29	27, 28	ax-mp 7	. . . . . 6 ⊢ suc ∅ ≠ ∅
30		df-ne 2203	. . . . . 6 ⊢ (suc ∅ ≠ ∅ ↔ ¬ suc ∅ = ∅)
31	29, 30	mpbi 133	. . . . 5 ⊢ ¬ suc ∅ = ∅
32		pm2.53 640	. . . . 5 ⊢ ((suc ∅ = ∅ ∨ φ) → (¬ suc ∅ = ∅ → φ))
33	31, 32	mpi 15	. . . 4 ⊢ ((suc ∅ = ∅ ∨ φ) → φ)
34	26, 33	sylbi 114	. . 3 ⊢ (suc ∅ ∈ {z ∈ {∅, {∅}} ∣ (z = ∅ ∨ φ)} → φ)
35	19	eqeq1i 2044	. . . . 5 ⊢ (suc ∅ = {z ∈ {∅, {∅}} ∣ (z = ∅ ∨ φ)} ↔ {∅} = {z ∈ {∅, {∅}} ∣ (z = ∅ ∨ φ)})
36	19	eqeq1i 2044	. . . . . . . 8 ⊢ (suc ∅ = ∅ ↔ {∅} = ∅)
37	31, 36	mtbi 594	. . . . . . 7 ⊢ ¬ {∅} = ∅
38	20	elsnc 3390	. . . . . . 7 ⊢ ({∅} ∈ {∅} ↔ {∅} = ∅)
39	37, 38	mtbir 595	. . . . . 6 ⊢ ¬ {∅} ∈ {∅}
40		eleq2 2098	. . . . . 6 ⊢ ({∅} = {z ∈ {∅, {∅}} ∣ (z = ∅ ∨ φ)} → ({∅} ∈ {∅} ↔ {∅} ∈ {z ∈ {∅, {∅}} ∣ (z = ∅ ∨ φ)}))
41	39, 40	mtbii 598	. . . . 5 ⊢ ({∅} = {z ∈ {∅, {∅}} ∣ (z = ∅ ∨ φ)} → ¬ {∅} ∈ {z ∈ {∅, {∅}} ∣ (z = ∅ ∨ φ)})
42	35, 41	sylbi 114	. . . 4 ⊢ (suc ∅ = {z ∈ {∅, {∅}} ∣ (z = ∅ ∨ φ)} → ¬ {∅} ∈ {z ∈ {∅, {∅}} ∣ (z = ∅ ∨ φ)})
43		olc 631	. . . . 5 ⊢ (φ → ({∅} = ∅ ∨ φ))
44		eqeq1 2043	. . . . . . . 8 ⊢ (z = {∅} → (z = ∅ ↔ {∅} = ∅))
45	44	orbi1d 704	. . . . . . 7 ⊢ (z = {∅} → ((z = ∅ ∨ φ) ↔ ({∅} = ∅ ∨ φ)))
46	45	elrab3 2693	. . . . . 6 ⊢ ({∅} ∈ {∅, {∅}} → ({∅} ∈ {z ∈ {∅, {∅}} ∣ (z = ∅ ∨ φ)} ↔ ({∅} = ∅ ∨ φ)))
47	21, 46	ax-mp 7	. . . . 5 ⊢ ({∅} ∈ {z ∈ {∅, {∅}} ∣ (z = ∅ ∨ φ)} ↔ ({∅} = ∅ ∨ φ))
48	43, 47	sylibr 137	. . . 4 ⊢ (φ → {∅} ∈ {z ∈ {∅, {∅}} ∣ (z = ∅ ∨ φ)})
49	42, 48	nsyl 558	. . 3 ⊢ (suc ∅ = {z ∈ {∅, {∅}} ∣ (z = ∅ ∨ φ)} → ¬ φ)
50	34, 49	orim12i 675	. 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 628   = wceq 1242   ∈ wcel 1390   ≠ wne 2201  ∀wral 2300  {crab 2304  Vcvv 2551  ∅c0 3218  {csn 3367  {cpr 3368  Oncon0 4066  suc csuc 4068

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 544  ax-in2 545  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bndl 1396  ax-4 1397  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-sep 3866  ax-nul 3874  ax-pow 3918

This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ne 2203  df-ral 2305  df-rex 2306  df-rab 2309  df-v 2553  df-dif 2914  df-un 2916  df-in 2918  df-ss 2925  df-nul 3219  df-pw 3353  df-sn 3373  df-pr 3374  df-uni 3572  df-tr 3846  df-iord 4069  df-on 4071  df-suc 4074

This theorem is referenced by:  ordsucunielexmid  4216