Theorem tgldimor

Description: Excluded-middle like statement allowing to treat dimension zero as a special case. (Contributed by Thierry Arnoux, 11-Apr-2019)

	Ref	Expression
Hypotheses	tgldimor.p	$$⊢P=E\left(F\right)$$
	tgldimor.a	$$⊢\phi \to A\in P$$
Assertion	tgldimor	$$⊢\phi \to \left(\left|P\right|=1\vee 2\le \left|P\right|\right)$$

Proof

Step	Hyp	Ref	Expression
1		tgldimor.p	$$⊢P=E\left(F\right)$$
2		tgldimor.a	$$⊢\phi \to A\in P$$
3	1	fvexi	$$⊢P\in \mathrm{V}$$
4		hashv01gt1	$$⊢P\in \mathrm{V}\to \left(\left|P\right|=0\vee \left|P\right|=1\vee 1<\left|P\right|\right)$$
5	3 4	ax-mp	$$⊢\left(\left|P\right|=0\vee \left|P\right|=1\vee 1<\left|P\right|\right)$$
6		3orass	$$⊢\left(\left|P\right|=0\vee \left|P\right|=1\vee 1<\left|P\right|\right)\leftrightarrow \left(\left|P\right|=0\vee \left(\left|P\right|=1\vee 1<\left|P\right|\right)\right)$$
7	5 6	mpbi	$$⊢\left(\left|P\right|=0\vee \left(\left|P\right|=1\vee 1<\left|P\right|\right)\right)$$
8		1p1e2	$$⊢1+1=2$$
9		1z	$$⊢1\in \mathbb{Z}$$
10		nn0z	$$⊢\left|P\right|\in {\mathbb{N}}_0\to \left|P\right|\in \mathbb{Z}$$
11		zltp1le	$$⊢\left(1\in \mathbb{Z}\wedge \left|P\right|\in \mathbb{Z}\right)\to \left(1<\left|P\right|\leftrightarrow 1+1\le \left|P\right|\right)$$
12	9 10 11	sylancr	$$⊢\left|P\right|\in {\mathbb{N}}_0\to \left(1<\left|P\right|\leftrightarrow 1+1\le \left|P\right|\right)$$
13	12	biimpac	$$⊢\left(1<\left|P\right|\wedge \left|P\right|\in {\mathbb{N}}_0\right)\to 1+1\le \left|P\right|$$
14	8 13	eqbrtrrid	$$⊢\left(1<\left|P\right|\wedge \left|P\right|\in {\mathbb{N}}_0\right)\to 2\le \left|P\right|$$
15		2re	$$⊢2\in ℝ$$
16	15	rexri	$$⊢2\in {ℝ}^{*}$$
17		pnfge	$$⊢2\in {ℝ}^{*}\to 2\le \mathrm{+\infty }$$
18	16 17	ax-mp	$$⊢2\le \mathrm{+\infty }$$
19		breq2	$$⊢\left|P\right|=\mathrm{+\infty }\to \left(2\le \left|P\right|\leftrightarrow 2\le \mathrm{+\infty }\right)$$
20	18 19	mpbiri	$$⊢\left|P\right|=\mathrm{+\infty }\to 2\le \left|P\right|$$
21	20	adantl	$$⊢\left(1<\left|P\right|\wedge \left|P\right|=\mathrm{+\infty }\right)\to 2\le \left|P\right|$$
22		hashnn0pnf	$$⊢P\in \mathrm{V}\to \left(\left|P\right|\in {\mathbb{N}}_0\vee \left|P\right|=\mathrm{+\infty }\right)$$
23	3 22	mp1i	$$⊢1<\left|P\right|\to \left(\left|P\right|\in {\mathbb{N}}_0\vee \left|P\right|=\mathrm{+\infty }\right)$$
24	14 21 23	mpjaodan	$$⊢1<\left|P\right|\to 2\le \left|P\right|$$
25	24	orim2i	$$⊢\left(\left|P\right|=1\vee 1<\left|P\right|\right)\to \left(\left|P\right|=1\vee 2\le \left|P\right|\right)$$
26	25	orim2i	$$⊢\left(\left|P\right|=0\vee \left(\left|P\right|=1\vee 1<\left|P\right|\right)\right)\to \left(\left|P\right|=0\vee \left(\left|P\right|=1\vee 2\le \left|P\right|\right)\right)$$
27	7 26	mp1i	$$⊢\phi \to \left(\left|P\right|=0\vee \left(\left|P\right|=1\vee 2\le \left|P\right|\right)\right)$$
28		ne0i	$$⊢A\in P\to P\ne \varnothing$$
29		hasheq0	$$⊢P\in \mathrm{V}\to \left(\left|P\right|=0\leftrightarrow P=\varnothing \right)$$
30	3 29	ax-mp	$$⊢\left|P\right|=0\leftrightarrow P=\varnothing$$
31	30	biimpi	$$⊢\left|P\right|=0\to P=\varnothing$$
32	31	necon3ai	$$⊢P\ne \varnothing \to \neg \left|P\right|=0$$
33	2 28 32	3syl	$$⊢\phi \to \neg \left|P\right|=0$$
34		biorf	$$⊢\neg \left|P\right|=0\to \left(\left(\left|P\right|=1\vee 2\le \left|P\right|\right)\leftrightarrow \left(\left|P\right|=0\vee \left(\left|P\right|=1\vee 2\le \left|P\right|\right)\right)\right)$$
35	33 34	syl	$$⊢\phi \to \left(\left(\left|P\right|=1\vee 2\le \left|P\right|\right)\leftrightarrow \left(\left|P\right|=0\vee \left(\left|P\right|=1\vee 2\le \left|P\right|\right)\right)\right)$$
36	27 35	mpbird	$$⊢\phi \to \left(\left|P\right|=1\vee 2\le \left|P\right|\right)$$