isarchi2

Description: Alternative way to express the predicate " W is Archimedean ", for Tosets. (Contributed by Thierry Arnoux, 30-Jan-2018)

	Ref	Expression
Hypotheses	isarchi2.b	$⊢ B = {Base}_{W}$
	isarchi2.0	$⊢ \underset{˙}{0} = 0_{W}$
	isarchi2.x	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
	isarchi2.l	$⊢ \underset{˙}{\leq} = \leq_{W}$
	isarchi2.t	$⊢ \underset{˙}{<} = <_{W}$
Assertion	isarchi2	$⊢ (W \in Toset \land W \in Mnd) \to (W \in Archi \leftrightarrow \forall x \in B \forall y \in B (\underset{˙}{0} \underset{˙}{<} x \to \exists n \in ℕ y \underset{˙}{\leq} (n \underset{˙}{\cdot} x)))$

Proof

Step	Hyp	Ref	Expression
1		isarchi2.b	$⊢ B = {Base}_{W}$
2		isarchi2.0	$⊢ \underset{˙}{0} = 0_{W}$
3		isarchi2.x	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
4		isarchi2.l	$⊢ \underset{˙}{\leq} = \leq_{W}$
5		isarchi2.t	$⊢ \underset{˙}{<} = <_{W}$
6		eqid	$⊢ ⋘ (W) = ⋘ (W)$
7	1 2 6	isarchi	$⊢ W \in Toset \to (W \in Archi \leftrightarrow \forall x \in B \forall y \in B \neg x ⋘ (W) y)$
8	7	adantr	$⊢ (W \in Toset \land W \in Mnd) \to (W \in Archi \leftrightarrow \forall x \in B \forall y \in B \neg x ⋘ (W) y)$
9		simpl1l	$⊢ (((W \in Toset \land W \in Mnd) \land x \in B \land y \in B) \land n \in ℕ) \to W \in Toset$
10		simpl1r	$⊢ (((W \in Toset \land W \in Mnd) \land x \in B \land y \in B) \land n \in ℕ) \to W \in Mnd$
11		simpr	$⊢ (((W \in Toset \land W \in Mnd) \land x \in B \land y \in B) \land n \in ℕ) \to n \in ℕ$
12	11	nnnn0d	$⊢ (((W \in Toset \land W \in Mnd) \land x \in B \land y \in B) \land n \in ℕ) \to n \in ℕ_{0}$
13		simpl2	$⊢ (((W \in Toset \land W \in Mnd) \land x \in B \land y \in B) \land n \in ℕ) \to x \in B$
14	1 3	mulgnn0cl	$⊢ (W \in Mnd \land n \in ℕ_{0} \land x \in B) \to n \underset{˙}{\cdot} x \in B$
15	10 12 13 14	syl3anc	$⊢ (((W \in Toset \land W \in Mnd) \land x \in B \land y \in B) \land n \in ℕ) \to n \underset{˙}{\cdot} x \in B$
16		simpl3	$⊢ (((W \in Toset \land W \in Mnd) \land x \in B \land y \in B) \land n \in ℕ) \to y \in B$
17	1 4 5	tltnle	$⊢ (W \in Toset \land n \underset{˙}{\cdot} x \in B \land y \in B) \to ((n \underset{˙}{\cdot} x) \underset{˙}{<} y \leftrightarrow \neg y \underset{˙}{\leq} (n \underset{˙}{\cdot} x))$
18	17	con2bid	$⊢ (W \in Toset \land n \underset{˙}{\cdot} x \in B \land y \in B) \to (y \underset{˙}{\leq} (n \underset{˙}{\cdot} x) \leftrightarrow \neg (n \underset{˙}{\cdot} x) \underset{˙}{<} y)$
19	9 15 16 18	syl3anc	$⊢ (((W \in Toset \land W \in Mnd) \land x \in B \land y \in B) \land n \in ℕ) \to (y \underset{˙}{\leq} (n \underset{˙}{\cdot} x) \leftrightarrow \neg (n \underset{˙}{\cdot} x) \underset{˙}{<} y)$
20	19	rexbidva	$⊢ ((W \in Toset \land W \in Mnd) \land x \in B \land y \in B) \to (\exists n \in ℕ y \underset{˙}{\leq} (n \underset{˙}{\cdot} x) \leftrightarrow \exists n \in ℕ \neg (n \underset{˙}{\cdot} x) \underset{˙}{<} y)$
21	20	imbi2d	$⊢ ((W \in Toset \land W \in Mnd) \land x \in B \land y \in B) \to ((\underset{˙}{0} \underset{˙}{<} x \to \exists n \in ℕ y \underset{˙}{\leq} (n \underset{˙}{\cdot} x)) \leftrightarrow (\underset{˙}{0} \underset{˙}{<} x \to \exists n \in ℕ \neg (n \underset{˙}{\cdot} x) \underset{˙}{<} y))$
22	1 2 3 5	isinftm	$⊢ (W \in Toset \land x \in B \land y \in B) \to (x ⋘ (W) y \leftrightarrow (\underset{˙}{0} \underset{˙}{<} x \land \forall n \in ℕ (n \underset{˙}{\cdot} x) \underset{˙}{<} y))$
23	22	notbid	$⊢ (W \in Toset \land x \in B \land y \in B) \to (\neg x ⋘ (W) y \leftrightarrow \neg (\underset{˙}{0} \underset{˙}{<} x \land \forall n \in ℕ (n \underset{˙}{\cdot} x) \underset{˙}{<} y))$
24		rexnal	$⊢ \exists n \in ℕ \neg (n \underset{˙}{\cdot} x) \underset{˙}{<} y \leftrightarrow \neg \forall n \in ℕ (n \underset{˙}{\cdot} x) \underset{˙}{<} y$
25	24	imbi2i	$⊢ (\underset{˙}{0} \underset{˙}{<} x \to \exists n \in ℕ \neg (n \underset{˙}{\cdot} x) \underset{˙}{<} y) \leftrightarrow (\underset{˙}{0} \underset{˙}{<} x \to \neg \forall n \in ℕ (n \underset{˙}{\cdot} x) \underset{˙}{<} y)$
26		imnan	$⊢ (\underset{˙}{0} \underset{˙}{<} x \to \neg \forall n \in ℕ (n \underset{˙}{\cdot} x) \underset{˙}{<} y) \leftrightarrow \neg (\underset{˙}{0} \underset{˙}{<} x \land \forall n \in ℕ (n \underset{˙}{\cdot} x) \underset{˙}{<} y)$
27	25 26	bitr2i	$⊢ \neg (\underset{˙}{0} \underset{˙}{<} x \land \forall n \in ℕ (n \underset{˙}{\cdot} x) \underset{˙}{<} y) \leftrightarrow (\underset{˙}{0} \underset{˙}{<} x \to \exists n \in ℕ \neg (n \underset{˙}{\cdot} x) \underset{˙}{<} y)$
28	23 27	bitrdi	$⊢ (W \in Toset \land x \in B \land y \in B) \to (\neg x ⋘ (W) y \leftrightarrow (\underset{˙}{0} \underset{˙}{<} x \to \exists n \in ℕ \neg (n \underset{˙}{\cdot} x) \underset{˙}{<} y))$
29	28	3adant1r	$⊢ ((W \in Toset \land W \in Mnd) \land x \in B \land y \in B) \to (\neg x ⋘ (W) y \leftrightarrow (\underset{˙}{0} \underset{˙}{<} x \to \exists n \in ℕ \neg (n \underset{˙}{\cdot} x) \underset{˙}{<} y))$
30	21 29	bitr4d	$⊢ ((W \in Toset \land W \in Mnd) \land x \in B \land y \in B) \to ((\underset{˙}{0} \underset{˙}{<} x \to \exists n \in ℕ y \underset{˙}{\leq} (n \underset{˙}{\cdot} x)) \leftrightarrow \neg x ⋘ (W) y)$
31	30	3expb	$⊢ ((W \in Toset \land W \in Mnd) \land (x \in B \land y \in B)) \to ((\underset{˙}{0} \underset{˙}{<} x \to \exists n \in ℕ y \underset{˙}{\leq} (n \underset{˙}{\cdot} x)) \leftrightarrow \neg x ⋘ (W) y)$
32	31	2ralbidva	$⊢ (W \in Toset \land W \in Mnd) \to (\forall x \in B \forall y \in B (\underset{˙}{0} \underset{˙}{<} x \to \exists n \in ℕ y \underset{˙}{\leq} (n \underset{˙}{\cdot} x)) \leftrightarrow \forall x \in B \forall y \in B \neg x ⋘ (W) y)$
33	8 32	bitr4d	$⊢ (W \in Toset \land W \in Mnd) \to (W \in Archi \leftrightarrow \forall x \in B \forall y \in B (\underset{˙}{0} \underset{˙}{<} x \to \exists n \in ℕ y \underset{˙}{\leq} (n \underset{˙}{\cdot} x)))$

Metamath Proof Explorer

Theorem isarchi2

Proof