Metamath Proof Explorer

Theorem zntoslem

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

Ref Expression
Hypotheses znle2.y ⊢ 𝑌 = ( ℤ/nℤ ‘ 𝑁 )
znle2.f ⊢ 𝐹 = ( ( ℤRHom ‘ 𝑌 ) ↾ 𝑊 )
znle2.w ⊢ 𝑊 = if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) )
znle2.l ⊢ ≤ = ( le ‘ 𝑌 )
znleval.x ⊢ 𝑋 = ( Base ‘ 𝑌 )
Assertion zntoslem ( 𝑁 ∈ ℕ0 → 𝑌 ∈ Toset )

Proof

Step Hyp Ref Expression
1 znle2.y ⊢ 𝑌 = ( ℤ/nℤ ‘ 𝑁 )
2 znle2.f ⊢ 𝐹 = ( ( ℤRHom ‘ 𝑌 ) ↾ 𝑊 )
3 znle2.w ⊢ 𝑊 = if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) )
4 znle2.l ⊢ ≤ = ( le ‘ 𝑌 )
5 znleval.x ⊢ 𝑋 = ( Base ‘ 𝑌 )
6 1 fvexi ⊢ 𝑌 ∈ V
7 6 a1i ⊢ ( 𝑁 ∈ ℕ0 → 𝑌 ∈ V )
8 5 a1i ⊢ ( 𝑁 ∈ ℕ0 → 𝑋 = ( Base ‘ 𝑌 ) )
9 4 a1i ⊢ ( 𝑁 ∈ ℕ0 → ≤ = ( le ‘ 𝑌 ) )
10 1 5 2 3 znf1o ⊢ ( 𝑁 ∈ ℕ0 → 𝐹 : 𝑊 –1-1-onto→ 𝑋 )
11 f1ocnv ⊢ ( 𝐹 : 𝑊 –1-1-onto→ 𝑋 → ◡ 𝐹 : 𝑋 –1-1-onto→ 𝑊 )
12 10 11 syl ⊢ ( 𝑁 ∈ ℕ0 → ◡ 𝐹 : 𝑋 –1-1-onto→ 𝑊 )
13 f1of ⊢ ( ◡ 𝐹 : 𝑋 –1-1-onto→ 𝑊 → ◡ 𝐹 : 𝑋 ⟶ 𝑊 )
14 12 13 syl ⊢ ( 𝑁 ∈ ℕ0 → ◡ 𝐹 : 𝑋 ⟶ 𝑊 )
15 sseq1 ⊢ ( ℤ = if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) ) → ( ℤ ⊆ ℤ ↔ if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) ) ⊆ ℤ ) )
16 sseq1 ⊢ ( ( 0 ..^ 𝑁 ) = if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) ) → ( ( 0 ..^ 𝑁 ) ⊆ ℤ ↔ if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) ) ⊆ ℤ ) )
17 ssid ⊢ ℤ ⊆ ℤ
18 fzossz ⊢ ( 0 ..^ 𝑁 ) ⊆ ℤ
19 15 16 17 18 keephyp ⊢ if ( 𝑁 = 0 , ℤ , ( 0 ..^ 𝑁 ) ) ⊆ ℤ
20 3 19 eqsstri ⊢ 𝑊 ⊆ ℤ
21 zssre ⊢ ℤ ⊆ ℝ
22 20 21 sstri ⊢ 𝑊 ⊆ ℝ
23 fss ⊢ ( ( ◡ 𝐹 : 𝑋 ⟶ 𝑊 ∧ 𝑊 ⊆ ℝ ) → ◡ 𝐹 : 𝑋 ⟶ ℝ )
24 14 22 23 sylancl ⊢ ( 𝑁 ∈ ℕ0 → ◡ 𝐹 : 𝑋 ⟶ ℝ )
25 24 ffvelcdmda ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ 𝑋 ) → ( ◡ 𝐹 ‘ 𝑥 ) ∈ ℝ )
26 25 leidd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ 𝑋 ) → ( ◡ 𝐹 ‘ 𝑥 ) ≤ ( ◡ 𝐹 ‘ 𝑥 ) )
27 1 2 3 4 5 znleval2 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑥 ≤ 𝑥 ↔ ( ◡ 𝐹 ‘ 𝑥 ) ≤ ( ◡ 𝐹 ‘ 𝑥 ) ) )
28 27 3anidm23 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑥 ≤ 𝑥 ↔ ( ◡ 𝐹 ‘ 𝑥 ) ≤ ( ◡ 𝐹 ‘ 𝑥 ) ) )
29 26 28 mpbird ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ≤ 𝑥 )
30 1 2 3 4 5 znleval2 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑥 ≤ 𝑦 ↔ ( ◡ 𝐹 ‘ 𝑥 ) ≤ ( ◡ 𝐹 ‘ 𝑦 ) ) )
31 1 2 3 4 5 znleval2 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑦 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑦 ≤ 𝑥 ↔ ( ◡ 𝐹 ‘ 𝑦 ) ≤ ( ◡ 𝐹 ‘ 𝑥 ) ) )
32 31 3com23 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑦 ≤ 𝑥 ↔ ( ◡ 𝐹 ‘ 𝑦 ) ≤ ( ◡ 𝐹 ‘ 𝑥 ) ) )
33 30 32 anbi12d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥 ) ↔ ( ( ◡ 𝐹 ‘ 𝑥 ) ≤ ( ◡ 𝐹 ‘ 𝑦 ) ∧ ( ◡ 𝐹 ‘ 𝑦 ) ≤ ( ◡ 𝐹 ‘ 𝑥 ) ) ) )
34 25 3adant3 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( ◡ 𝐹 ‘ 𝑥 ) ∈ ℝ )
35 24 ffvelcdmda ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑦 ∈ 𝑋 ) → ( ◡ 𝐹 ‘ 𝑦 ) ∈ ℝ )
36 35 3adant2 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( ◡ 𝐹 ‘ 𝑦 ) ∈ ℝ )
37 34 36 letri3d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( ( ◡ 𝐹 ‘ 𝑥 ) = ( ◡ 𝐹 ‘ 𝑦 ) ↔ ( ( ◡ 𝐹 ‘ 𝑥 ) ≤ ( ◡ 𝐹 ‘ 𝑦 ) ∧ ( ◡ 𝐹 ‘ 𝑦 ) ≤ ( ◡ 𝐹 ‘ 𝑥 ) ) ) )
38 f1of1 ⊢ ( ◡ 𝐹 : 𝑋 –1-1-onto→ 𝑊 → ◡ 𝐹 : 𝑋 –1-1→ 𝑊 )
39 12 38 syl ⊢ ( 𝑁 ∈ ℕ0 → ◡ 𝐹 : 𝑋 –1-1→ 𝑊 )
40 f1fveq ⊢ ( ( ◡ 𝐹 : 𝑋 –1-1→ 𝑊 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( ◡ 𝐹 ‘ 𝑥 ) = ( ◡ 𝐹 ‘ 𝑦 ) ↔ 𝑥 = 𝑦 ) )
41 39 40 sylan ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( ◡ 𝐹 ‘ 𝑥 ) = ( ◡ 𝐹 ‘ 𝑦 ) ↔ 𝑥 = 𝑦 ) )
42 41 3impb ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( ( ◡ 𝐹 ‘ 𝑥 ) = ( ◡ 𝐹 ‘ 𝑦 ) ↔ 𝑥 = 𝑦 ) )
43 33 37 42 3bitr2d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥 ) ↔ 𝑥 = 𝑦 ) )
44 43 biimpd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑥 ) → 𝑥 = 𝑦 ) )
45 25 3ad2antr1 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( ◡ 𝐹 ‘ 𝑥 ) ∈ ℝ )
46 35 3ad2antr2 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( ◡ 𝐹 ‘ 𝑦 ) ∈ ℝ )
47 24 ffvelcdmda ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑧 ∈ 𝑋 ) → ( ◡ 𝐹 ‘ 𝑧 ) ∈ ℝ )
48 47 3ad2antr3 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( ◡ 𝐹 ‘ 𝑧 ) ∈ ℝ )
49 letr ⊢ ( ( ( ◡ 𝐹 ‘ 𝑥 ) ∈ ℝ ∧ ( ◡ 𝐹 ‘ 𝑦 ) ∈ ℝ ∧ ( ◡ 𝐹 ‘ 𝑧 ) ∈ ℝ ) → ( ( ( ◡ 𝐹 ‘ 𝑥 ) ≤ ( ◡ 𝐹 ‘ 𝑦 ) ∧ ( ◡ 𝐹 ‘ 𝑦 ) ≤ ( ◡ 𝐹 ‘ 𝑧 ) ) → ( ◡ 𝐹 ‘ 𝑥 ) ≤ ( ◡ 𝐹 ‘ 𝑧 ) ) )
50 45 46 48 49 syl3anc ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( ( ( ◡ 𝐹 ‘ 𝑥 ) ≤ ( ◡ 𝐹 ‘ 𝑦 ) ∧ ( ◡ 𝐹 ‘ 𝑦 ) ≤ ( ◡ 𝐹 ‘ 𝑧 ) ) → ( ◡ 𝐹 ‘ 𝑥 ) ≤ ( ◡ 𝐹 ‘ 𝑧 ) ) )
51 30 3adant3r3 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( 𝑥 ≤ 𝑦 ↔ ( ◡ 𝐹 ‘ 𝑥 ) ≤ ( ◡ 𝐹 ‘ 𝑦 ) ) )
52 1 2 3 4 5 znleval2 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) → ( 𝑦 ≤ 𝑧 ↔ ( ◡ 𝐹 ‘ 𝑦 ) ≤ ( ◡ 𝐹 ‘ 𝑧 ) ) )
53 52 3adant3r1 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( 𝑦 ≤ 𝑧 ↔ ( ◡ 𝐹 ‘ 𝑦 ) ≤ ( ◡ 𝐹 ‘ 𝑧 ) ) )
54 51 53 anbi12d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧 ) ↔ ( ( ◡ 𝐹 ‘ 𝑥 ) ≤ ( ◡ 𝐹 ‘ 𝑦 ) ∧ ( ◡ 𝐹 ‘ 𝑦 ) ≤ ( ◡ 𝐹 ‘ 𝑧 ) ) ) )
55 1 2 3 4 5 znleval2 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) → ( 𝑥 ≤ 𝑧 ↔ ( ◡ 𝐹 ‘ 𝑥 ) ≤ ( ◡ 𝐹 ‘ 𝑧 ) ) )
56 55 3adant3r2 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( 𝑥 ≤ 𝑧 ↔ ( ◡ 𝐹 ‘ 𝑥 ) ≤ ( ◡ 𝐹 ‘ 𝑧 ) ) )
57 50 54 56 3imtr4d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( ( 𝑥 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧 ) → 𝑥 ≤ 𝑧 ) )
58 7 8 9 29 44 57 isposd ⊢ ( 𝑁 ∈ ℕ0 → 𝑌 ∈ Poset )
59 34 36 letrid ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( ( ◡ 𝐹 ‘ 𝑥 ) ≤ ( ◡ 𝐹 ‘ 𝑦 ) ∨ ( ◡ 𝐹 ‘ 𝑦 ) ≤ ( ◡ 𝐹 ‘ 𝑥 ) ) )
60 30 32 orbi12d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( ( 𝑥 ≤ 𝑦 ∨ 𝑦 ≤ 𝑥 ) ↔ ( ( ◡ 𝐹 ‘ 𝑥 ) ≤ ( ◡ 𝐹 ‘ 𝑦 ) ∨ ( ◡ 𝐹 ‘ 𝑦 ) ≤ ( ◡ 𝐹 ‘ 𝑥 ) ) ) )
61 59 60 mpbird ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑥 ≤ 𝑦 ∨ 𝑦 ≤ 𝑥 ) )
62 61 3expb ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 ≤ 𝑦 ∨ 𝑦 ≤ 𝑥 ) )
63 62 ralrimivva ⊢ ( 𝑁 ∈ ℕ0 → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 ≤ 𝑦 ∨ 𝑦 ≤ 𝑥 ) )
64 5 4 istos ⊢ ( 𝑌 ∈ Toset ↔ ( 𝑌 ∈ Poset ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 ≤ 𝑦 ∨ 𝑦 ≤ 𝑥 ) ) )
65 58 63 64 sylanbrc ⊢ ( 𝑁 ∈ ℕ0 → 𝑌 ∈ Toset )