Theorem ordtriexmid 4479

Description: Ordinal trichotomy implies the law of the excluded middle (that is, decidability of an arbitrary proposition).

This theorem is stated in "Constructive ordinals", [Crosilla], p. "Set-theoretic principles incompatible with intuitionistic logic".

(Contributed by Mario Carneiro and Jim Kingdon, 14-Nov-2018.)

Hypothesis

Ref	Expression
ordtriexmid.1	|- A. x e. On A. y e. On ( x e. y \/ x = y \/ y e. x )

Assertion

Ref	Expression
ordtriexmid	|- ( ph \/ -. ph )

Distinct variable groups:   x, y   ph, x

Allowed substitution hint:   ph( y)

Proof of Theorem ordtriexmid

Dummy variable z is distinct from all other variables.

Step	Hyp	Ref	Expression
1		noel 3398	. . . 4 |- -. { z e. { (/) } | ph } e. (/)
2		ordtriexmidlem 4477	. . . . . 6 |- { z e. { (/) } | ph } e. On
3		eleq1 2220	. . . . . . . 8 |- ( x = { z e. { (/) } | ph } -> ( x e. (/) <-> { z e. { (/) } | ph } e. (/) ) )
4		eqeq1 2164	. . . . . . . 8 |- ( x = { z e. { (/) } | ph } -> ( x = (/) <-> { z e. { (/) } | ph } = (/) ) )
5		eleq2 2221	. . . . . . . 8 |- ( x = { z e. { (/) } | ph } -> ( (/) e. x <-> (/) e. { z e. { (/) } | ph } ) )
6	3, 4, 5	3orbi123d 1293	. . . . . . 7 |- ( x = { z e. { (/) } | ph } -> ( ( x e. (/) \/ x = (/) \/ (/) e. x ) <-> ( { z e. { (/) } | ph } e. (/) \/ { z e. { (/) } | ph } = (/) \/ (/) e. { z e. { (/) } | ph } ) ) )
7		0elon 4352	. . . . . . . 8 |- (/) e. On
8		0ex 4091	. . . . . . . . 9 |- (/) e. _V
9		eleq1 2220	. . . . . . . . . . 11 |- ( y = (/) -> ( y e. On <-> (/) e. On ) )
10	9	anbi2d 460	. . . . . . . . . 10 |- ( y = (/) -> ( ( x e. On /\ y e. On ) <-> ( x e. On /\ (/) e. On ) ) )
11		eleq2 2221	. . . . . . . . . . 11 |- ( y = (/) -> ( x e. y <-> x e. (/) ) )
12		eqeq2 2167	. . . . . . . . . . 11 |- ( y = (/) -> ( x = y <-> x = (/) ) )
13		eleq1 2220	. . . . . . . . . . 11 |- ( y = (/) -> ( y e. x <-> (/) e. x ) )
14	11, 12, 13	3orbi123d 1293	. . . . . . . . . 10 |- ( y = (/) -> ( ( x e. y \/ x = y \/ y e. x ) <-> ( x e. (/) \/ x = (/) \/ (/) e. x ) ) )
15	10, 14	imbi12d 233	. . . . . . . . 9 |- ( y = (/) -> ( ( ( x e. On /\ y e. On ) -> ( x e. y \/ x = y \/ y e. x ) ) <-> ( ( x e. On /\ (/) e. On ) -> ( x e. (/) \/ x = (/) \/ (/) e. x ) ) ) )
16		ordtriexmid.1	. . . . . . . . . 10 |- A. x e. On A. y e. On ( x e. y \/ x = y \/ y e. x )
17	16	rspec2 2546	. . . . . . . . 9 |- ( ( x e. On /\ y e. On ) -> ( x e. y \/ x = y \/ y e. x ) )
18	8, 15, 17	vtocl 2766	. . . . . . . 8 |- ( ( x e. On /\ (/) e. On ) -> ( x e. (/) \/ x = (/) \/ (/) e. x ) )
19	7, 18	mpan2 422	. . . . . . 7 |- ( x e. On -> ( x e. (/) \/ x = (/) \/ (/) e. x ) )
20	6, 19	vtoclga 2778	. . . . . 6 |- ( { z e. { (/) } | ph } e. On -> ( { z e. { (/) } | ph } e. (/) \/ { z e. { (/) } | ph } = (/) \/ (/) e. { z e. { (/) } | ph } ) )
21	2, 20	ax-mp 5	. . . . 5 |- ( { z e. { (/) } | ph } e. (/) \/ { z e. { (/) } | ph } = (/) \/ (/) e. { z e. { (/) } | ph } )
22		3orass 966	. . . . 5 |- ( ( { z e. { (/) } | ph } e. (/) \/ { z e. { (/) } | ph } = (/) \/ (/) e. { z e. { (/) } | ph } ) <-> ( { z e. { (/) } | ph } e. (/) \/ ( { z e. { (/) } | ph } = (/) \/ (/) e. { z e. { (/) } | ph } ) ) )
23	21, 22	mpbi 144	. . . 4 |- ( { z e. { (/) } | ph } e. (/) \/ ( { z e. { (/) } | ph } = (/) \/ (/) e. { z e. { (/) } | ph } ) )
24	1, 23	mtpor 1407	. . 3 |- ( { z e. { (/) } | ph } = (/) \/ (/) e. { z e. { (/) } | ph } )
25		ordtriexmidlem2 4478	. . . 4 |- ( { z e. { (/) } | ph } = (/) -> -. ph )
26	8	snid 3591	. . . . . 6 |- (/) e. { (/) }
27		biidd 171	. . . . . . 7 |- ( z = (/) -> ( ph <-> ph ) )
28	27	elrab3 2869	. . . . . 6 |- ( (/) e. { (/) } -> ( (/) e. { z e. { (/) } | ph } <-> ph ) )
29	26, 28	ax-mp 5	. . . . 5 |- ( (/) e. { z e. { (/) } | ph } <-> ph )
30	29	biimpi 119	. . . 4 |- ( (/) e. { z e. { (/) } | ph } -> ph )
31	25, 30	orim12i 749	. . 3 |- ( ( { z e. { (/) } | ph } = (/) \/ (/) e. { z e. { (/) } | ph } ) -> ( -. ph \/ ph ) )
32	24, 31	ax-mp 5	. 2 |- ( -. ph \/ ph )
33		orcom 718	. 2 |- ( ( ph \/ -. ph ) <-> ( -. ph \/ ph ) )
34	32, 33	mpbir 145	1 |- ( ph \/ -. ph )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 103   <-> wb 104   \/ wo 698   \/ w3o 962   = wceq 1335   e. wcel 2128   A.wral 2435   {crab 2439   (/)c0 3394   {csn 3560   Oncon0 4323

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-14 2131  ax-ext 2139  ax-sep 4082  ax-nul 4090  ax-pow 4135

This theorem depends on definitions:  df-bi 116  df-3or 964  df-3an 965  df-tru 1338  df-nf 1441  df-sb 1743  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-ral 2440  df-rex 2441  df-rab 2444  df-v 2714  df-dif 3104  df-un 3106  df-in 3108  df-ss 3115  df-nul 3395  df-pw 3545  df-sn 3566  df-uni 3773  df-tr 4063  df-iord 4326  df-on 4328  df-suc 4331

This theorem is referenced by: (None)