Theorem isinftm

Description: Express x is infinitesimal with respect to y for a structure W . (Contributed by Thierry Arnoux, 30-Jan-2018)

	Ref	Expression
Hypotheses	inftm.b	$$⊢B={\mathrm{Base}}_W$$
	inftm.0	$$⊢\underset{\dot{}}{0}=0_W$$
	inftm.x	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
	inftm.l	$$⊢\underset{\dot{}}{<}={<}_W$$
Assertion	isinftm	$$⊢\left(W\in V\wedge X\in B\wedge Y\in B\right)\to \left(X⋘\left(W\right)Y\leftrightarrow \left(\underset{\dot{}}{0}\underset{\dot{}}{<}X\wedge \forall n\in \mathbb{N}\left(n\underset{\dot{}}{·}X\right)\underset{\dot{}}{<}Y\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		inftm.b	$$⊢B={\mathrm{Base}}_W$$
2		inftm.0	$$⊢\underset{\dot{}}{0}=0_W$$
3		inftm.x	$$⊢\underset{\dot{}}{·}={\cdot }_W$$
4		inftm.l	$$⊢\underset{\dot{}}{<}={<}_W$$
5		eleq1	$$⊢x=X\to \left(x\in B\leftrightarrow X\in B\right)$$
6		eleq1	$$⊢y=Y\to \left(y\in B\leftrightarrow Y\in B\right)$$
7	5 6	bi2anan9	$$⊢\left(x=X\wedge y=Y\right)\to \left(\left(x\in B\wedge y\in B\right)\leftrightarrow \left(X\in B\wedge Y\in B\right)\right)$$
8		simpl	$$⊢\left(x=X\wedge y=Y\right)\to x=X$$
9	8	breq2d	$$⊢\left(x=X\wedge y=Y\right)\to \left(\underset{\dot{}}{0}\underset{\dot{}}{<}x\leftrightarrow \underset{\dot{}}{0}\underset{\dot{}}{<}X\right)$$
10	8	oveq2d	$$⊢\left(x=X\wedge y=Y\right)\to n\underset{\dot{}}{·}x=n\underset{\dot{}}{·}X$$
11		simpr	$$⊢\left(x=X\wedge y=Y\right)\to y=Y$$
12	10 11	breq12d	$$⊢\left(x=X\wedge y=Y\right)\to \left(\left(n\underset{\dot{}}{·}x\right)\underset{\dot{}}{<}y\leftrightarrow \left(n\underset{\dot{}}{·}X\right)\underset{\dot{}}{<}Y\right)$$
13	12	ralbidv	$$⊢\left(x=X\wedge y=Y\right)\to \left(\forall n\in \mathbb{N}\left(n\underset{\dot{}}{·}x\right)\underset{\dot{}}{<}y\leftrightarrow \forall n\in \mathbb{N}\left(n\underset{\dot{}}{·}X\right)\underset{\dot{}}{<}Y\right)$$
14	9 13	anbi12d	$$⊢\left(x=X\wedge y=Y\right)\to \left(\left(\underset{\dot{}}{0}\underset{\dot{}}{<}x\wedge \forall n\in \mathbb{N}\left(n\underset{\dot{}}{·}x\right)\underset{\dot{}}{<}y\right)\leftrightarrow \left(\underset{\dot{}}{0}\underset{\dot{}}{<}X\wedge \forall n\in \mathbb{N}\left(n\underset{\dot{}}{·}X\right)\underset{\dot{}}{<}Y\right)\right)$$
15	7 14	anbi12d	$$⊢\left(x=X\wedge y=Y\right)\to \left(\left(\left(x\in B\wedge y\in B\right)\wedge \left(\underset{\dot{}}{0}\underset{\dot{}}{<}x\wedge \forall n\in \mathbb{N}\left(n\underset{\dot{}}{·}x\right)\underset{\dot{}}{<}y\right)\right)\leftrightarrow \left(\left(X\in B\wedge Y\in B\right)\wedge \left(\underset{\dot{}}{0}\underset{\dot{}}{<}X\wedge \forall n\in \mathbb{N}\left(n\underset{\dot{}}{·}X\right)\underset{\dot{}}{<}Y\right)\right)\right)$$
16		eqid	$$⊢\left\{⟨x,y⟩|\left(\left(x\in B\wedge y\in B\right)\wedge \left(\underset{\dot{}}{0}\underset{\dot{}}{<}x\wedge \forall n\in \mathbb{N}\left(n\underset{\dot{}}{·}x\right)\underset{\dot{}}{<}y\right)\right)\right\}=\left\{⟨x,y⟩|\left(\left(x\in B\wedge y\in B\right)\wedge \left(\underset{\dot{}}{0}\underset{\dot{}}{<}x\wedge \forall n\in \mathbb{N}\left(n\underset{\dot{}}{·}x\right)\underset{\dot{}}{<}y\right)\right)\right\}$$
17	15 16	brabga	$$⊢\left(X\in B\wedge Y\in B\right)\to \left(X\left\{⟨x,y⟩|\left(\left(x\in B\wedge y\in B\right)\wedge \left(\underset{\dot{}}{0}\underset{\dot{}}{<}x\wedge \forall n\in \mathbb{N}\left(n\underset{\dot{}}{·}x\right)\underset{\dot{}}{<}y\right)\right)\right\}Y\leftrightarrow \left(\left(X\in B\wedge Y\in B\right)\wedge \left(\underset{\dot{}}{0}\underset{\dot{}}{<}X\wedge \forall n\in \mathbb{N}\left(n\underset{\dot{}}{·}X\right)\underset{\dot{}}{<}Y\right)\right)\right)$$
18	17	3adant1	$$⊢\left(W\in V\wedge X\in B\wedge Y\in B\right)\to \left(X\left\{⟨x,y⟩|\left(\left(x\in B\wedge y\in B\right)\wedge \left(\underset{\dot{}}{0}\underset{\dot{}}{<}x\wedge \forall n\in \mathbb{N}\left(n\underset{\dot{}}{·}x\right)\underset{\dot{}}{<}y\right)\right)\right\}Y\leftrightarrow \left(\left(X\in B\wedge Y\in B\right)\wedge \left(\underset{\dot{}}{0}\underset{\dot{}}{<}X\wedge \forall n\in \mathbb{N}\left(n\underset{\dot{}}{·}X\right)\underset{\dot{}}{<}Y\right)\right)\right)$$
19		elex	$$⊢W\in V\to W\in \mathrm{V}$$
20	19	3ad2ant1	$$⊢\left(W\in V\wedge X\in B\wedge Y\in B\right)\to W\in \mathrm{V}$$
21		fveq2	$$⊢w=W\to {\mathrm{Base}}_w={\mathrm{Base}}_W$$
22	21 1	eqtr4di	$$⊢w=W\to {\mathrm{Base}}_w=B$$
23	22	eleq2d	$$⊢w=W\to \left(x\in {\mathrm{Base}}_w\leftrightarrow x\in B\right)$$
24	22	eleq2d	$$⊢w=W\to \left(y\in {\mathrm{Base}}_w\leftrightarrow y\in B\right)$$
25	23 24	anbi12d	$$⊢w=W\to \left(\left(x\in {\mathrm{Base}}_w\wedge y\in {\mathrm{Base}}_w\right)\leftrightarrow \left(x\in B\wedge y\in B\right)\right)$$
26		fveq2	$$⊢w=W\to 0_w=0_W$$
27	26 2	eqtr4di	$$⊢w=W\to 0_w=\underset{\dot{}}{0}$$
28		fveq2	$$⊢w=W\to {<}_w={<}_W$$
29	28 4	eqtr4di	$$⊢w=W\to {<}_w=\underset{\dot{}}{<}$$
30		eqidd	$$⊢w=W\to x=x$$
31	27 29 30	breq123d	$$⊢w=W\to \left(0_w{<}_{w}x\leftrightarrow \underset{\dot{}}{0}\underset{\dot{}}{<}x\right)$$
32		fveq2	$$⊢w=W\to {\cdot }_w={\cdot }_W$$
33	32 3	eqtr4di	$$⊢w=W\to {\cdot }_w=\underset{\dot{}}{·}$$
34	33	oveqd	$$⊢w=W\to n{\cdot }_{w}x=n\underset{\dot{}}{·}x$$
35		eqidd	$$⊢w=W\to y=y$$
36	34 29 35	breq123d	$$⊢w=W\to \left(\left(n{\cdot }_{w}x\right){<}_{w}y\leftrightarrow \left(n\underset{\dot{}}{·}x\right)\underset{\dot{}}{<}y\right)$$
37	36	ralbidv	$$⊢w=W\to \left(\forall n\in \mathbb{N}\left(n{\cdot }_{w}x\right){<}_{w}y\leftrightarrow \forall n\in \mathbb{N}\left(n\underset{\dot{}}{·}x\right)\underset{\dot{}}{<}y\right)$$
38	31 37	anbi12d	$$⊢w=W\to \left(\left(0_w{<}_{w}x\wedge \forall n\in \mathbb{N}\left(n{\cdot }_{w}x\right){<}_{w}y\right)\leftrightarrow \left(\underset{\dot{}}{0}\underset{\dot{}}{<}x\wedge \forall n\in \mathbb{N}\left(n\underset{\dot{}}{·}x\right)\underset{\dot{}}{<}y\right)\right)$$
39	25 38	anbi12d	$$⊢w=W\to \left(\left(\left(x\in {\mathrm{Base}}_w\wedge y\in {\mathrm{Base}}_w\right)\wedge \left(0_w{<}_{w}x\wedge \forall n\in \mathbb{N}\left(n{\cdot }_{w}x\right){<}_{w}y\right)\right)\leftrightarrow \left(\left(x\in B\wedge y\in B\right)\wedge \left(\underset{\dot{}}{0}\underset{\dot{}}{<}x\wedge \forall n\in \mathbb{N}\left(n\underset{\dot{}}{·}x\right)\underset{\dot{}}{<}y\right)\right)\right)$$
40	39	opabbidv	$$⊢w=W\to \left\{⟨x,y⟩|\left(\left(x\in {\mathrm{Base}}_w\wedge y\in {\mathrm{Base}}_w\right)\wedge \left(0_w{<}_{w}x\wedge \forall n\in \mathbb{N}\left(n{\cdot }_{w}x\right){<}_{w}y\right)\right)\right\}=\left\{⟨x,y⟩|\left(\left(x\in B\wedge y\in B\right)\wedge \left(\underset{\dot{}}{0}\underset{\dot{}}{<}x\wedge \forall n\in \mathbb{N}\left(n\underset{\dot{}}{·}x\right)\underset{\dot{}}{<}y\right)\right)\right\}$$
41		df-inftm	$$⊢⋘=\left(w\in \mathrm{V}⟼\left\{⟨x,y⟩|\left(\left(x\in {\mathrm{Base}}_w\wedge y\in {\mathrm{Base}}_w\right)\wedge \left(0_w{<}_{w}x\wedge \forall n\in \mathbb{N}\left(n{\cdot }_{w}x\right){<}_{w}y\right)\right)\right\}\right)$$
42	1	fvexi	$$⊢B\in \mathrm{V}$$
43	42 42	xpex	$$⊢B\times B\in \mathrm{V}$$
44		opabssxp	$$⊢\left\{⟨x,y⟩|\left(\left(x\in B\wedge y\in B\right)\wedge \left(\underset{\dot{}}{0}\underset{\dot{}}{<}x\wedge \forall n\in \mathbb{N}\left(n\underset{\dot{}}{·}x\right)\underset{\dot{}}{<}y\right)\right)\right\}\subseteq B\times B$$
45	43 44	ssexi	$$⊢\left\{⟨x,y⟩|\left(\left(x\in B\wedge y\in B\right)\wedge \left(\underset{\dot{}}{0}\underset{\dot{}}{<}x\wedge \forall n\in \mathbb{N}\left(n\underset{\dot{}}{·}x\right)\underset{\dot{}}{<}y\right)\right)\right\}\in \mathrm{V}$$
46	40 41 45	fvmpt	$$⊢W\in \mathrm{V}\to ⋘\left(W\right)=\left\{⟨x,y⟩|\left(\left(x\in B\wedge y\in B\right)\wedge \left(\underset{\dot{}}{0}\underset{\dot{}}{<}x\wedge \forall n\in \mathbb{N}\left(n\underset{\dot{}}{·}x\right)\underset{\dot{}}{<}y\right)\right)\right\}$$
47	20 46	syl	$$⊢\left(W\in V\wedge X\in B\wedge Y\in B\right)\to ⋘\left(W\right)=\left\{⟨x,y⟩|\left(\left(x\in B\wedge y\in B\right)\wedge \left(\underset{\dot{}}{0}\underset{\dot{}}{<}x\wedge \forall n\in \mathbb{N}\left(n\underset{\dot{}}{·}x\right)\underset{\dot{}}{<}y\right)\right)\right\}$$
48	47	breqd	$$⊢\left(W\in V\wedge X\in B\wedge Y\in B\right)\to \left(X⋘\left(W\right)Y\leftrightarrow X\left\{⟨x,y⟩|\left(\left(x\in B\wedge y\in B\right)\wedge \left(\underset{\dot{}}{0}\underset{\dot{}}{<}x\wedge \forall n\in \mathbb{N}\left(n\underset{\dot{}}{·}x\right)\underset{\dot{}}{<}y\right)\right)\right\}Y\right)$$
49		3simpc	$$⊢\left(W\in V\wedge X\in B\wedge Y\in B\right)\to \left(X\in B\wedge Y\in B\right)$$
50	49	biantrurd	$$⊢\left(W\in V\wedge X\in B\wedge Y\in B\right)\to \left(\left(\underset{\dot{}}{0}\underset{\dot{}}{<}X\wedge \forall n\in \mathbb{N}\left(n\underset{\dot{}}{·}X\right)\underset{\dot{}}{<}Y\right)\leftrightarrow \left(\left(X\in B\wedge Y\in B\right)\wedge \left(\underset{\dot{}}{0}\underset{\dot{}}{<}X\wedge \forall n\in \mathbb{N}\left(n\underset{\dot{}}{·}X\right)\underset{\dot{}}{<}Y\right)\right)\right)$$
51	18 48 50	3bitr4d	$$⊢\left(W\in V\wedge X\in B\wedge Y\in B\right)\to \left(X⋘\left(W\right)Y\leftrightarrow \left(\underset{\dot{}}{0}\underset{\dot{}}{<}X\wedge \forall n\in \mathbb{N}\left(n\underset{\dot{}}{·}X\right)\underset{\dot{}}{<}Y\right)\right)$$