zntoslem

Description: Lemma for zntos . (Contributed by Mario Carneiro, 15-Jun-2015) (Revised by AV, 13-Jun-2019)

	Ref	Expression
Hypotheses	znle2.y	$⊢ Y = ℤ / N ℤ$
	znle2.f	$⊢ F = {ℤRHom (Y) ↾}_{W}$
	znle2.w	$⊢ W = if (N = 0, ℤ, (0 ..^N))$
	znle2.l	$⊢ \underset{˙}{\leq} = \leq_{Y}$
	znleval.x	$⊢ X = {Base}_{Y}$
Assertion	zntoslem	$⊢ N \in ℕ_{0} \to Y \in Toset$

Proof

Step	Hyp	Ref	Expression
1		znle2.y	$⊢ Y = ℤ / N ℤ$
2		znle2.f	$⊢ F = {ℤRHom (Y) ↾}_{W}$
3		znle2.w	$⊢ W = if (N = 0, ℤ, (0 ..^N))$
4		znle2.l	$⊢ \underset{˙}{\leq} = \leq_{Y}$
5		znleval.x	$⊢ X = {Base}_{Y}$
6	1	fvexi	$⊢ Y \in V$
7	6	a1i	$⊢ N \in ℕ_{0} \to Y \in V$
8	5	a1i	$⊢ N \in ℕ_{0} \to X = {Base}_{Y}$
9	4	a1i	$⊢ N \in ℕ_{0} \to \underset{˙}{\leq} = \leq_{Y}$
10	1 5 2 3	znf1o	$⊢ N \in ℕ_{0} \to F : W \underset{1-1 onto}{⟶} X$
11		f1ocnv	$⊢ F : W \underset{1-1 onto}{⟶} X \to F^{-1} : X \underset{1-1 onto}{⟶} W$
12	10 11	syl	$⊢ N \in ℕ_{0} \to F^{-1} : X \underset{1-1 onto}{⟶} W$
13		f1of	$⊢ F^{-1} : X \underset{1-1 onto}{⟶} W \to F^{-1} : X ⟶ W$
14	12 13	syl	$⊢ N \in ℕ_{0} \to F^{-1} : X ⟶ W$
15		sseq1	$⊢ ℤ = if (N = 0, ℤ, (0 ..^N)) \to (ℤ \subseteq ℤ \leftrightarrow if (N = 0, ℤ, (0 ..^N)) \subseteq ℤ)$
16		sseq1	$⊢ (0 ..^N) = if (N = 0, ℤ, (0 ..^N)) \to ((0 ..^N) \subseteq ℤ \leftrightarrow if (N = 0, ℤ, (0 ..^N)) \subseteq ℤ)$
17		ssid	$⊢ ℤ \subseteq ℤ$
18		fzossz	$⊢ (0 ..^N) \subseteq ℤ$
19	15 16 17 18	keephyp	$⊢ if (N = 0, ℤ, (0 ..^N)) \subseteq ℤ$
20	3 19	eqsstri	$⊢ W \subseteq ℤ$
21		zssre	$⊢ ℤ \subseteq ℝ$
22	20 21	sstri	$⊢ W \subseteq ℝ$
23		fss	$⊢ (F^{-1} : X ⟶ W \land W \subseteq ℝ) \to F^{-1} : X ⟶ ℝ$
24	14 22 23	sylancl	$⊢ N \in ℕ_{0} \to F^{-1} : X ⟶ ℝ$
25	24	ffvelcdmda	$⊢ (N \in ℕ_{0} \land x \in X) \to F^{-1} (x) \in ℝ$
26	25	leidd	$⊢ (N \in ℕ_{0} \land x \in X) \to F^{-1} (x) \leq F^{-1} (x)$
27	1 2 3 4 5	znleval2	$⊢ (N \in ℕ_{0} \land x \in X \land x \in X) \to (x \underset{˙}{\leq} x \leftrightarrow F^{-1} (x) \leq F^{-1} (x))$
28	27	3anidm23	$⊢ (N \in ℕ_{0} \land x \in X) \to (x \underset{˙}{\leq} x \leftrightarrow F^{-1} (x) \leq F^{-1} (x))$
29	26 28	mpbird	$⊢ (N \in ℕ_{0} \land x \in X) \to x \underset{˙}{\leq} x$
30	1 2 3 4 5	znleval2	$⊢ (N \in ℕ_{0} \land x \in X \land y \in X) \to (x \underset{˙}{\leq} y \leftrightarrow F^{-1} (x) \leq F^{-1} (y))$
31	1 2 3 4 5	znleval2	$⊢ (N \in ℕ_{0} \land y \in X \land x \in X) \to (y \underset{˙}{\leq} x \leftrightarrow F^{-1} (y) \leq F^{-1} (x))$
32	31	3com23	$⊢ (N \in ℕ_{0} \land x \in X \land y \in X) \to (y \underset{˙}{\leq} x \leftrightarrow F^{-1} (y) \leq F^{-1} (x))$
33	30 32	anbi12d	$⊢ (N \in ℕ_{0} \land x \in X \land y \in X) \to ((x \underset{˙}{\leq} y \land y \underset{˙}{\leq} x) \leftrightarrow (F^{-1} (x) \leq F^{-1} (y) \land F^{-1} (y) \leq F^{-1} (x)))$
34	25	3adant3	$⊢ (N \in ℕ_{0} \land x \in X \land y \in X) \to F^{-1} (x) \in ℝ$
35	24	ffvelcdmda	$⊢ (N \in ℕ_{0} \land y \in X) \to F^{-1} (y) \in ℝ$
36	35	3adant2	$⊢ (N \in ℕ_{0} \land x \in X \land y \in X) \to F^{-1} (y) \in ℝ$
37	34 36	letri3d	$⊢ (N \in ℕ_{0} \land x \in X \land y \in X) \to (F^{-1} (x) = F^{-1} (y) \leftrightarrow (F^{-1} (x) \leq F^{-1} (y) \land F^{-1} (y) \leq F^{-1} (x)))$
38		f1of1	$⊢ F^{-1} : X \underset{1-1 onto}{⟶} W \to F^{-1} : X \underset{1-1}{⟶} W$
39	12 38	syl	$⊢ N \in ℕ_{0} \to F^{-1} : X \underset{1-1}{⟶} W$
40		f1fveq	$⊢ (F^{-1} : X \underset{1-1}{⟶} W \land (x \in X \land y \in X)) \to (F^{-1} (x) = F^{-1} (y) \leftrightarrow x = y)$
41	39 40	sylan	$⊢ (N \in ℕ_{0} \land (x \in X \land y \in X)) \to (F^{-1} (x) = F^{-1} (y) \leftrightarrow x = y)$
42	41	3impb	$⊢ (N \in ℕ_{0} \land x \in X \land y \in X) \to (F^{-1} (x) = F^{-1} (y) \leftrightarrow x = y)$
43	33 37 42	3bitr2d	$⊢ (N \in ℕ_{0} \land x \in X \land y \in X) \to ((x \underset{˙}{\leq} y \land y \underset{˙}{\leq} x) \leftrightarrow x = y)$
44	43	biimpd	$⊢ (N \in ℕ_{0} \land x \in X \land y \in X) \to ((x \underset{˙}{\leq} y \land y \underset{˙}{\leq} x) \to x = y)$
45	25	3ad2antr1	$⊢ (N \in ℕ_{0} \land (x \in X \land y \in X \land z \in X)) \to F^{-1} (x) \in ℝ$
46	35	3ad2antr2	$⊢ (N \in ℕ_{0} \land (x \in X \land y \in X \land z \in X)) \to F^{-1} (y) \in ℝ$
47	24	ffvelcdmda	$⊢ (N \in ℕ_{0} \land z \in X) \to F^{-1} (z) \in ℝ$
48	47	3ad2antr3	$⊢ (N \in ℕ_{0} \land (x \in X \land y \in X \land z \in X)) \to F^{-1} (z) \in ℝ$
49		letr	$⊢ (F^{-1} (x) \in ℝ \land F^{-1} (y) \in ℝ \land F^{-1} (z) \in ℝ) \to ((F^{-1} (x) \leq F^{-1} (y) \land F^{-1} (y) \leq F^{-1} (z)) \to F^{-1} (x) \leq F^{-1} (z))$
50	45 46 48 49	syl3anc	$⊢ (N \in ℕ_{0} \land (x \in X \land y \in X \land z \in X)) \to ((F^{-1} (x) \leq F^{-1} (y) \land F^{-1} (y) \leq F^{-1} (z)) \to F^{-1} (x) \leq F^{-1} (z))$
51	30	3adant3r3	$⊢ (N \in ℕ_{0} \land (x \in X \land y \in X \land z \in X)) \to (x \underset{˙}{\leq} y \leftrightarrow F^{-1} (x) \leq F^{-1} (y))$
52	1 2 3 4 5	znleval2	$⊢ (N \in ℕ_{0} \land y \in X \land z \in X) \to (y \underset{˙}{\leq} z \leftrightarrow F^{-1} (y) \leq F^{-1} (z))$
53	52	3adant3r1	$⊢ (N \in ℕ_{0} \land (x \in X \land y \in X \land z \in X)) \to (y \underset{˙}{\leq} z \leftrightarrow F^{-1} (y) \leq F^{-1} (z))$
54	51 53	anbi12d	$⊢ (N \in ℕ_{0} \land (x \in X \land y \in X \land z \in X)) \to ((x \underset{˙}{\leq} y \land y \underset{˙}{\leq} z) \leftrightarrow (F^{-1} (x) \leq F^{-1} (y) \land F^{-1} (y) \leq F^{-1} (z)))$
55	1 2 3 4 5	znleval2	$⊢ (N \in ℕ_{0} \land x \in X \land z \in X) \to (x \underset{˙}{\leq} z \leftrightarrow F^{-1} (x) \leq F^{-1} (z))$
56	55	3adant3r2	$⊢ (N \in ℕ_{0} \land (x \in X \land y \in X \land z \in X)) \to (x \underset{˙}{\leq} z \leftrightarrow F^{-1} (x) \leq F^{-1} (z))$
57	50 54 56	3imtr4d	$⊢ (N \in ℕ_{0} \land (x \in X \land y \in X \land z \in X)) \to ((x \underset{˙}{\leq} y \land y \underset{˙}{\leq} z) \to x \underset{˙}{\leq} z)$
58	7 8 9 29 44 57	isposd	$⊢ N \in ℕ_{0} \to Y \in Poset$
59	34 36	letrid	$⊢ (N \in ℕ_{0} \land x \in X \land y \in X) \to (F^{-1} (x) \leq F^{-1} (y) \lor F^{-1} (y) \leq F^{-1} (x))$
60	30 32	orbi12d	$⊢ (N \in ℕ_{0} \land x \in X \land y \in X) \to ((x \underset{˙}{\leq} y \lor y \underset{˙}{\leq} x) \leftrightarrow (F^{-1} (x) \leq F^{-1} (y) \lor F^{-1} (y) \leq F^{-1} (x)))$
61	59 60	mpbird	$⊢ (N \in ℕ_{0} \land x \in X \land y \in X) \to (x \underset{˙}{\leq} y \lor y \underset{˙}{\leq} x)$
62	61	3expb	$⊢ (N \in ℕ_{0} \land (x \in X \land y \in X)) \to (x \underset{˙}{\leq} y \lor y \underset{˙}{\leq} x)$
63	62	ralrimivva	$⊢ N \in ℕ_{0} \to \forall x \in X \forall y \in X (x \underset{˙}{\leq} y \lor y \underset{˙}{\leq} x)$
64	5 4	istos	$⊢ Y \in Toset \leftrightarrow (Y \in Poset \land \forall x \in X \forall y \in X (x \underset{˙}{\leq} y \lor y \underset{˙}{\leq} x))$
65	58 63 64	sylanbrc	$⊢ N \in ℕ_{0} \to Y \in Toset$

Metamath Proof Explorer

Theorem zntoslem

Proof