Theorem odfval

Description: Value of the order function. For a shorter proof using ax-rep , see odfvalALT . (Contributed by Mario Carneiro, 13-Jul-2014) (Revised by AV, 5-Oct-2020) Remove dependency on ax-rep . (Revised by Rohan Ridenour, 17-Aug-2023)

	Ref	Expression
Hypotheses	odval.1	$$⊢X={\mathrm{Base}}_G$$
	odval.2	$$⊢\underset{\dot{}}{·}={\cdot }_G$$
	odval.3	$$⊢\underset{\dot{}}{0}=0_G$$
	odval.4	$$⊢O=\mathrm{od}\left(G\right)$$
Assertion	odfval	$$⊢O=\left(x\in X⟼⦋\left\{y\in \mathbb{N}|y\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\}/i⦌if\left(i=\varnothing ,0,inf\left(i,ℝ,<\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		odval.1	$$⊢X={\mathrm{Base}}_G$$
2		odval.2	$$⊢\underset{\dot{}}{·}={\cdot }_G$$
3		odval.3	$$⊢\underset{\dot{}}{0}=0_G$$
4		odval.4	$$⊢O=\mathrm{od}\left(G\right)$$
5		fveq2	$$⊢g=G\to {\mathrm{Base}}_g={\mathrm{Base}}_G$$
6	5 1	eqtr4di	$$⊢g=G\to {\mathrm{Base}}_g=X$$
7		fveq2	$$⊢g=G\to {\cdot }_g={\cdot }_G$$
8	7 2	eqtr4di	$$⊢g=G\to {\cdot }_g=\underset{\dot{}}{·}$$
9	8	oveqd	$$⊢g=G\to y{\cdot }_{g}x=y\underset{\dot{}}{·}x$$
10		fveq2	$$⊢g=G\to 0_g=0_G$$
11	10 3	eqtr4di	$$⊢g=G\to 0_g=\underset{\dot{}}{0}$$
12	9 11	eqeq12d	$$⊢g=G\to \left(y{\cdot }_{g}x=0_g\leftrightarrow y\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right)$$
13	12	rabbidv	$$⊢g=G\to \left\{y\in \mathbb{N}|y{\cdot }_{g}x=0_g\right\}=\left\{y\in \mathbb{N}|y\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\}$$
14	13	csbeq1d	$$⊢g=G\to ⦋\left\{y\in \mathbb{N}|y{\cdot }_{g}x=0_g\right\}/i⦌if\left(i=\varnothing ,0,inf\left(i,ℝ,<\right)\right)=⦋\left\{y\in \mathbb{N}|y\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\}/i⦌if\left(i=\varnothing ,0,inf\left(i,ℝ,<\right)\right)$$
15	6 14	mpteq12dv	$$⊢g=G\to \left(x\in {\mathrm{Base}}_g⟼⦋\left\{y\in \mathbb{N}|y{\cdot }_{g}x=0_g\right\}/i⦌if\left(i=\varnothing ,0,inf\left(i,ℝ,<\right)\right)\right)=\left(x\in X⟼⦋\left\{y\in \mathbb{N}|y\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\}/i⦌if\left(i=\varnothing ,0,inf\left(i,ℝ,<\right)\right)\right)$$
16		df-od	$$⊢\mathrm{od}=\left(g\in \mathrm{V}⟼\left(x\in {\mathrm{Base}}_g⟼⦋\left\{y\in \mathbb{N}|y{\cdot }_{g}x=0_g\right\}/i⦌if\left(i=\varnothing ,0,inf\left(i,ℝ,<\right)\right)\right)\right)$$
17	1	fvexi	$$⊢X\in \mathrm{V}$$
18		nn0ex	$$⊢{\mathbb{N}}_0\in \mathrm{V}$$
19		nnex	$$⊢\mathbb{N}\in \mathrm{V}$$
20	19	rabex	$$⊢\left\{y\in \mathbb{N}|y\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\}\in \mathrm{V}$$
21		eqeq1	$$⊢i=\left\{y\in \mathbb{N}|y\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\}\to \left(i=\varnothing \leftrightarrow \left\{y\in \mathbb{N}|y\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\}=\varnothing \right)$$
22		infeq1	$$⊢i=\left\{y\in \mathbb{N}|y\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\}\to inf\left(i,ℝ,<\right)=inf\left(\left\{y\in \mathbb{N}|y\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\},ℝ,<\right)$$
23	21 22	ifbieq2d	$$⊢i=\left\{y\in \mathbb{N}|y\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\}\to if\left(i=\varnothing ,0,inf\left(i,ℝ,<\right)\right)=if\left(\left\{y\in \mathbb{N}|y\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\}=\varnothing ,0,inf\left(\left\{y\in \mathbb{N}|y\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\},ℝ,<\right)\right)$$
24	20 23	csbie	$$⊢⦋\left\{y\in \mathbb{N}|y\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\}/i⦌if\left(i=\varnothing ,0,inf\left(i,ℝ,<\right)\right)=if\left(\left\{y\in \mathbb{N}|y\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\}=\varnothing ,0,inf\left(\left\{y\in \mathbb{N}|y\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\},ℝ,<\right)\right)$$
25		0nn0	$$⊢0\in {\mathbb{N}}_0$$
26	25	a1i	$$⊢\left(\top \wedge \left\{y\in \mathbb{N}|y\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\}=\varnothing \right)\to 0\in {\mathbb{N}}_0$$
27		df-ne	$$⊢\left\{y\in \mathbb{N}|y\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\}\ne \varnothing \leftrightarrow \neg \left\{y\in \mathbb{N}|y\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\}=\varnothing$$
28		ssrab2	$$⊢\left\{y\in \mathbb{N}|y\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\}\subseteq \mathbb{N}$$
29		nnuz	$$⊢\mathbb{N}={\mathbb{Z}}_{\ge 1}$$
30	28 29	sseqtri	$$⊢\left\{y\in \mathbb{N}|y\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\}\subseteq {\mathbb{Z}}_{\ge 1}$$
31		infssuzcl	$$⊢\left(\left\{y\in \mathbb{N}|y\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\}\subseteq {\mathbb{Z}}_{\ge 1}\wedge \left\{y\in \mathbb{N}|y\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\}\ne \varnothing \right)\to inf\left(\left\{y\in \mathbb{N}|y\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\},ℝ,<\right)\in \left\{y\in \mathbb{N}|y\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\}$$
32	30 31	mpan	$$⊢\left\{y\in \mathbb{N}|y\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\}\ne \varnothing \to inf\left(\left\{y\in \mathbb{N}|y\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\},ℝ,<\right)\in \left\{y\in \mathbb{N}|y\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\}$$
33	28 32	sselid	$$⊢\left\{y\in \mathbb{N}|y\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\}\ne \varnothing \to inf\left(\left\{y\in \mathbb{N}|y\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\},ℝ,<\right)\in \mathbb{N}$$
34	27 33	sylbir	$$⊢\neg \left\{y\in \mathbb{N}|y\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\}=\varnothing \to inf\left(\left\{y\in \mathbb{N}|y\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\},ℝ,<\right)\in \mathbb{N}$$
35	34	nnnn0d	$$⊢\neg \left\{y\in \mathbb{N}|y\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\}=\varnothing \to inf\left(\left\{y\in \mathbb{N}|y\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\},ℝ,<\right)\in {\mathbb{N}}_0$$
36	35	adantl	$$⊢\left(\top \wedge \neg \left\{y\in \mathbb{N}|y\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\}=\varnothing \right)\to inf\left(\left\{y\in \mathbb{N}|y\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\},ℝ,<\right)\in {\mathbb{N}}_0$$
37	26 36	ifclda	$$⊢\top \to if\left(\left\{y\in \mathbb{N}|y\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\}=\varnothing ,0,inf\left(\left\{y\in \mathbb{N}|y\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\},ℝ,<\right)\right)\in {\mathbb{N}}_0$$
38	37	mptru	$$⊢if\left(\left\{y\in \mathbb{N}|y\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\}=\varnothing ,0,inf\left(\left\{y\in \mathbb{N}|y\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\},ℝ,<\right)\right)\in {\mathbb{N}}_0$$
39	24 38	eqeltri	$$⊢⦋\left\{y\in \mathbb{N}|y\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\}/i⦌if\left(i=\varnothing ,0,inf\left(i,ℝ,<\right)\right)\in {\mathbb{N}}_0$$
40	39	rgenw	$$⊢\forall x\in X⦋\left\{y\in \mathbb{N}|y\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\}/i⦌if\left(i=\varnothing ,0,inf\left(i,ℝ,<\right)\right)\in {\mathbb{N}}_0$$
41	17 18 40	mptexw	$$⊢\left(x\in X⟼⦋\left\{y\in \mathbb{N}|y\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\}/i⦌if\left(i=\varnothing ,0,inf\left(i,ℝ,<\right)\right)\right)\in \mathrm{V}$$
42	15 16 41	fvmpt	$$⊢G\in \mathrm{V}\to \mathrm{od}\left(G\right)=\left(x\in X⟼⦋\left\{y\in \mathbb{N}|y\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\}/i⦌if\left(i=\varnothing ,0,inf\left(i,ℝ,<\right)\right)\right)$$
43		fvprc	$$⊢\neg G\in \mathrm{V}\to \mathrm{od}\left(G\right)=\varnothing$$
44		fvprc	$$⊢\neg G\in \mathrm{V}\to {\mathrm{Base}}_G=\varnothing$$
45	1 44	eqtrid	$$⊢\neg G\in \mathrm{V}\to X=\varnothing$$
46	45	mpteq1d	$$⊢\neg G\in \mathrm{V}\to \left(x\in X⟼⦋\left\{y\in \mathbb{N}|y\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\}/i⦌if\left(i=\varnothing ,0,inf\left(i,ℝ,<\right)\right)\right)=\left(x\in \varnothing ⟼⦋\left\{y\in \mathbb{N}|y\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\}/i⦌if\left(i=\varnothing ,0,inf\left(i,ℝ,<\right)\right)\right)$$
47		mpt0	$$⊢\left(x\in \varnothing ⟼⦋\left\{y\in \mathbb{N}|y\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\}/i⦌if\left(i=\varnothing ,0,inf\left(i,ℝ,<\right)\right)\right)=\varnothing$$
48	46 47	eqtrdi	$$⊢\neg G\in \mathrm{V}\to \left(x\in X⟼⦋\left\{y\in \mathbb{N}|y\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\}/i⦌if\left(i=\varnothing ,0,inf\left(i,ℝ,<\right)\right)\right)=\varnothing$$
49	43 48	eqtr4d	$$⊢\neg G\in \mathrm{V}\to \mathrm{od}\left(G\right)=\left(x\in X⟼⦋\left\{y\in \mathbb{N}|y\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\}/i⦌if\left(i=\varnothing ,0,inf\left(i,ℝ,<\right)\right)\right)$$
50	42 49	pm2.61i	$$⊢\mathrm{od}\left(G\right)=\left(x\in X⟼⦋\left\{y\in \mathbb{N}|y\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\}/i⦌if\left(i=\varnothing ,0,inf\left(i,ℝ,<\right)\right)\right)$$
51	4 50	eqtri	$$⊢O=\left(x\in X⟼⦋\left\{y\in \mathbb{N}|y\underset{\dot{}}{·}x=\underset{\dot{}}{0}\right\}/i⦌if\left(i=\varnothing ,0,inf\left(i,ℝ,<\right)\right)\right)$$