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 10 12 13	mulgnn0cld	$⊢ (((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$
15		simpl3	$⊢ (((W \in Toset \land W \in Mnd) \land x \in B \land y \in B) \land n \in ℕ) \to y \in B$
16	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))$
17	16	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)$
18	9 14 15 17	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)$
19	18	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)$
20	19	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))$
21	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))$
22	21	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))$
23		rexnal	$⊢ \exists n \in ℕ \neg (n \underset{˙}{\cdot} x) \underset{˙}{<} y \leftrightarrow \neg \forall n \in ℕ (n \underset{˙}{\cdot} x) \underset{˙}{<} y$
24	23	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)$
25		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)$
26	24 25	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)$
27	22 26	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))$
28	27	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))$
29	20 28	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)$
30	29	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)$
31	30	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)$
32	8 31	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