Metamath Proof Explorer

Theorem erdsze2lem1

Description: Lemma for erdsze2 . (Contributed by Mario Carneiro, 22-Jan-2015)

Ref Expression
Hypotheses erdsze2.r ⊢ ( 𝜑 → 𝑅 ∈ ℕ )
erdsze2.s ⊢ ( 𝜑 → 𝑆 ∈ ℕ )
erdsze2.f ⊢ ( 𝜑 → 𝐹 : 𝐴 –1-1→ ℝ )
erdsze2.a ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
erdsze2lem.n ⊢ 𝑁 = ( ( 𝑅 − 1 ) · ( 𝑆 − 1 ) )
erdsze2lem.l ⊢ ( 𝜑 → 𝑁 < ( ♯ ‘ 𝐴 ) )
Assertion erdsze2lem1 ( 𝜑 → ∃ 𝑓 ( 𝑓 : ( 1 ... ( 𝑁 + 1 ) ) –1-1→ 𝐴 ∧ 𝑓 Isom < , < ( ( 1 ... ( 𝑁 + 1 ) ) , ran 𝑓 ) ) )

Proof

Step Hyp Ref Expression
1 erdsze2.r ⊢ ( 𝜑 → 𝑅 ∈ ℕ )
2 erdsze2.s ⊢ ( 𝜑 → 𝑆 ∈ ℕ )
3 erdsze2.f ⊢ ( 𝜑 → 𝐹 : 𝐴 –1-1→ ℝ )
4 erdsze2.a ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
5 erdsze2lem.n ⊢ 𝑁 = ( ( 𝑅 − 1 ) · ( 𝑆 − 1 ) )
6 erdsze2lem.l ⊢ ( 𝜑 → 𝑁 < ( ♯ ‘ 𝐴 ) )
7 nnm1nn0 ⊢ ( 𝑅 ∈ ℕ → ( 𝑅 − 1 ) ∈ ℕ0 )
8 1 7 syl ⊢ ( 𝜑 → ( 𝑅 − 1 ) ∈ ℕ0 )
9 nnm1nn0 ⊢ ( 𝑆 ∈ ℕ → ( 𝑆 − 1 ) ∈ ℕ0 )
10 2 9 syl ⊢ ( 𝜑 → ( 𝑆 − 1 ) ∈ ℕ0 )
11 8 10 nn0mulcld ⊢ ( 𝜑 → ( ( 𝑅 − 1 ) · ( 𝑆 − 1 ) ) ∈ ℕ0 )
12 5 11 eqeltrid ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
13 peano2nn0 ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℕ0 )
14 hashfz1 ⊢ ( ( 𝑁 + 1 ) ∈ ℕ0 → ( ♯ ‘ ( 1 ... ( 𝑁 + 1 ) ) ) = ( 𝑁 + 1 ) )
15 12 13 14 3syl ⊢ ( 𝜑 → ( ♯ ‘ ( 1 ... ( 𝑁 + 1 ) ) ) = ( 𝑁 + 1 ) )
16 15 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ∈ Fin ) → ( ♯ ‘ ( 1 ... ( 𝑁 + 1 ) ) ) = ( 𝑁 + 1 ) )
17 6 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ∈ Fin ) → 𝑁 < ( ♯ ‘ 𝐴 ) )
18 hashcl ⊢ ( 𝐴 ∈ Fin → ( ♯ ‘ 𝐴 ) ∈ ℕ0 )
19 nn0ltp1le ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ0 ) → ( 𝑁 < ( ♯ ‘ 𝐴 ) ↔ ( 𝑁 + 1 ) ≤ ( ♯ ‘ 𝐴 ) ) )
20 12 18 19 syl2an ⊢ ( ( 𝜑 ∧ 𝐴 ∈ Fin ) → ( 𝑁 < ( ♯ ‘ 𝐴 ) ↔ ( 𝑁 + 1 ) ≤ ( ♯ ‘ 𝐴 ) ) )
21 17 20 mpbid ⊢ ( ( 𝜑 ∧ 𝐴 ∈ Fin ) → ( 𝑁 + 1 ) ≤ ( ♯ ‘ 𝐴 ) )
22 16 21 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝐴 ∈ Fin ) → ( ♯ ‘ ( 1 ... ( 𝑁 + 1 ) ) ) ≤ ( ♯ ‘ 𝐴 ) )
23 fzfid ⊢ ( ( 𝜑 ∧ 𝐴 ∈ Fin ) → ( 1 ... ( 𝑁 + 1 ) ) ∈ Fin )
24 simpr ⊢ ( ( 𝜑 ∧ 𝐴 ∈ Fin ) → 𝐴 ∈ Fin )
25 hashdom ⊢ ( ( ( 1 ... ( 𝑁 + 1 ) ) ∈ Fin ∧ 𝐴 ∈ Fin ) → ( ( ♯ ‘ ( 1 ... ( 𝑁 + 1 ) ) ) ≤ ( ♯ ‘ 𝐴 ) ↔ ( 1 ... ( 𝑁 + 1 ) ) ≼ 𝐴 ) )
26 23 24 25 syl2anc ⊢ ( ( 𝜑 ∧ 𝐴 ∈ Fin ) → ( ( ♯ ‘ ( 1 ... ( 𝑁 + 1 ) ) ) ≤ ( ♯ ‘ 𝐴 ) ↔ ( 1 ... ( 𝑁 + 1 ) ) ≼ 𝐴 ) )
27 22 26 mpbid ⊢ ( ( 𝜑 ∧ 𝐴 ∈ Fin ) → ( 1 ... ( 𝑁 + 1 ) ) ≼ 𝐴 )
28 simpr ⊢ ( ( 𝜑 ∧ ¬ 𝐴 ∈ Fin ) → ¬ 𝐴 ∈ Fin )
29 fzfid ⊢ ( ( 𝜑 ∧ ¬ 𝐴 ∈ Fin ) → ( 1 ... ( 𝑁 + 1 ) ) ∈ Fin )
30 isinffi ⊢ ( ( ¬ 𝐴 ∈ Fin ∧ ( 1 ... ( 𝑁 + 1 ) ) ∈ Fin ) → ∃ 𝑓 𝑓 : ( 1 ... ( 𝑁 + 1 ) ) –1-1→ 𝐴 )
31 28 29 30 syl2anc ⊢ ( ( 𝜑 ∧ ¬ 𝐴 ∈ Fin ) → ∃ 𝑓 𝑓 : ( 1 ... ( 𝑁 + 1 ) ) –1-1→ 𝐴 )
32 reex ⊢ ℝ ∈ V
33 ssexg ⊢ ( ( 𝐴 ⊆ ℝ ∧ ℝ ∈ V ) → 𝐴 ∈ V )
34 4 32 33 sylancl ⊢ ( 𝜑 → 𝐴 ∈ V )
35 34 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐴 ∈ Fin ) → 𝐴 ∈ V )
36 brdomg ⊢ ( 𝐴 ∈ V → ( ( 1 ... ( 𝑁 + 1 ) ) ≼ 𝐴 ↔ ∃ 𝑓 𝑓 : ( 1 ... ( 𝑁 + 1 ) ) –1-1→ 𝐴 ) )
37 35 36 syl ⊢ ( ( 𝜑 ∧ ¬ 𝐴 ∈ Fin ) → ( ( 1 ... ( 𝑁 + 1 ) ) ≼ 𝐴 ↔ ∃ 𝑓 𝑓 : ( 1 ... ( 𝑁 + 1 ) ) –1-1→ 𝐴 ) )
38 31 37 mpbird ⊢ ( ( 𝜑 ∧ ¬ 𝐴 ∈ Fin ) → ( 1 ... ( 𝑁 + 1 ) ) ≼ 𝐴 )
39 27 38 pm2.61dan ⊢ ( 𝜑 → ( 1 ... ( 𝑁 + 1 ) ) ≼ 𝐴 )
40 domeng ⊢ ( 𝐴 ∈ V → ( ( 1 ... ( 𝑁 + 1 ) ) ≼ 𝐴 ↔ ∃ 𝑠 ( ( 1 ... ( 𝑁 + 1 ) ) ≈ 𝑠 ∧ 𝑠 ⊆ 𝐴 ) ) )
41 34 40 syl ⊢ ( 𝜑 → ( ( 1 ... ( 𝑁 + 1 ) ) ≼ 𝐴 ↔ ∃ 𝑠 ( ( 1 ... ( 𝑁 + 1 ) ) ≈ 𝑠 ∧ 𝑠 ⊆ 𝐴 ) ) )
42 39 41 mpbid ⊢ ( 𝜑 → ∃ 𝑠 ( ( 1 ... ( 𝑁 + 1 ) ) ≈ 𝑠 ∧ 𝑠 ⊆ 𝐴 ) )
43 simprr ⊢ ( ( 𝜑 ∧ ( ( 1 ... ( 𝑁 + 1 ) ) ≈ 𝑠 ∧ 𝑠 ⊆ 𝐴 ) ) → 𝑠 ⊆ 𝐴 )
44 4 adantr ⊢ ( ( 𝜑 ∧ ( ( 1 ... ( 𝑁 + 1 ) ) ≈ 𝑠 ∧ 𝑠 ⊆ 𝐴 ) ) → 𝐴 ⊆ ℝ )
45 43 44 sstrd ⊢ ( ( 𝜑 ∧ ( ( 1 ... ( 𝑁 + 1 ) ) ≈ 𝑠 ∧ 𝑠 ⊆ 𝐴 ) ) → 𝑠 ⊆ ℝ )
46 ltso ⊢ < Or ℝ
47 soss ⊢ ( 𝑠 ⊆ ℝ → ( < Or ℝ → < Or 𝑠 ) )
48 45 46 47 mpisyl ⊢ ( ( 𝜑 ∧ ( ( 1 ... ( 𝑁 + 1 ) ) ≈ 𝑠 ∧ 𝑠 ⊆ 𝐴 ) ) → < Or 𝑠 )
49 fzfid ⊢ ( ( 𝜑 ∧ ( ( 1 ... ( 𝑁 + 1 ) ) ≈ 𝑠 ∧ 𝑠 ⊆ 𝐴 ) ) → ( 1 ... ( 𝑁 + 1 ) ) ∈ Fin )
50 simprl ⊢ ( ( 𝜑 ∧ ( ( 1 ... ( 𝑁 + 1 ) ) ≈ 𝑠 ∧ 𝑠 ⊆ 𝐴 ) ) → ( 1 ... ( 𝑁 + 1 ) ) ≈ 𝑠 )
51 enfi ⊢ ( ( 1 ... ( 𝑁 + 1 ) ) ≈ 𝑠 → ( ( 1 ... ( 𝑁 + 1 ) ) ∈ Fin ↔ 𝑠 ∈ Fin ) )
52 50 51 syl ⊢ ( ( 𝜑 ∧ ( ( 1 ... ( 𝑁 + 1 ) ) ≈ 𝑠 ∧ 𝑠 ⊆ 𝐴 ) ) → ( ( 1 ... ( 𝑁 + 1 ) ) ∈ Fin ↔ 𝑠 ∈ Fin ) )
53 49 52 mpbid ⊢ ( ( 𝜑 ∧ ( ( 1 ... ( 𝑁 + 1 ) ) ≈ 𝑠 ∧ 𝑠 ⊆ 𝐴 ) ) → 𝑠 ∈ Fin )
54 fz1iso ⊢ ( ( < Or 𝑠 ∧ 𝑠 ∈ Fin ) → ∃ 𝑓 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑠 ) ) , 𝑠 ) )
55 48 53 54 syl2anc ⊢ ( ( 𝜑 ∧ ( ( 1 ... ( 𝑁 + 1 ) ) ≈ 𝑠 ∧ 𝑠 ⊆ 𝐴 ) ) → ∃ 𝑓 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑠 ) ) , 𝑠 ) )
56 isof1o ⊢ ( 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑠 ) ) , 𝑠 ) → 𝑓 : ( 1 ... ( ♯ ‘ 𝑠 ) ) –1-1-onto→ 𝑠 )
57 56 adantl ⊢ ( ( ( 𝜑 ∧ ( ( 1 ... ( 𝑁 + 1 ) ) ≈ 𝑠 ∧ 𝑠 ⊆ 𝐴 ) ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑠 ) ) , 𝑠 ) ) → 𝑓 : ( 1 ... ( ♯ ‘ 𝑠 ) ) –1-1-onto→ 𝑠 )
58 hashen ⊢ ( ( ( 1 ... ( 𝑁 + 1 ) ) ∈ Fin ∧ 𝑠 ∈ Fin ) → ( ( ♯ ‘ ( 1 ... ( 𝑁 + 1 ) ) ) = ( ♯ ‘ 𝑠 ) ↔ ( 1 ... ( 𝑁 + 1 ) ) ≈ 𝑠 ) )
59 49 53 58 syl2anc ⊢ ( ( 𝜑 ∧ ( ( 1 ... ( 𝑁 + 1 ) ) ≈ 𝑠 ∧ 𝑠 ⊆ 𝐴 ) ) → ( ( ♯ ‘ ( 1 ... ( 𝑁 + 1 ) ) ) = ( ♯ ‘ 𝑠 ) ↔ ( 1 ... ( 𝑁 + 1 ) ) ≈ 𝑠 ) )
60 50 59 mpbird ⊢ ( ( 𝜑 ∧ ( ( 1 ... ( 𝑁 + 1 ) ) ≈ 𝑠 ∧ 𝑠 ⊆ 𝐴 ) ) → ( ♯ ‘ ( 1 ... ( 𝑁 + 1 ) ) ) = ( ♯ ‘ 𝑠 ) )
61 15 adantr ⊢ ( ( 𝜑 ∧ ( ( 1 ... ( 𝑁 + 1 ) ) ≈ 𝑠 ∧ 𝑠 ⊆ 𝐴 ) ) → ( ♯ ‘ ( 1 ... ( 𝑁 + 1 ) ) ) = ( 𝑁 + 1 ) )
62 60 61 eqtr3d ⊢ ( ( 𝜑 ∧ ( ( 1 ... ( 𝑁 + 1 ) ) ≈ 𝑠 ∧ 𝑠 ⊆ 𝐴 ) ) → ( ♯ ‘ 𝑠 ) = ( 𝑁 + 1 ) )
63 62 adantr ⊢ ( ( ( 𝜑 ∧ ( ( 1 ... ( 𝑁 + 1 ) ) ≈ 𝑠 ∧ 𝑠 ⊆ 𝐴 ) ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑠 ) ) , 𝑠 ) ) → ( ♯ ‘ 𝑠 ) = ( 𝑁 + 1 ) )
64 63 oveq2d ⊢ ( ( ( 𝜑 ∧ ( ( 1 ... ( 𝑁 + 1 ) ) ≈ 𝑠 ∧ 𝑠 ⊆ 𝐴 ) ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑠 ) ) , 𝑠 ) ) → ( 1 ... ( ♯ ‘ 𝑠 ) ) = ( 1 ... ( 𝑁 + 1 ) ) )
65 64 f1oeq2d ⊢ ( ( ( 𝜑 ∧ ( ( 1 ... ( 𝑁 + 1 ) ) ≈ 𝑠 ∧ 𝑠 ⊆ 𝐴 ) ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑠 ) ) , 𝑠 ) ) → ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑠 ) ) –1-1-onto→ 𝑠 ↔ 𝑓 : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ 𝑠 ) )
66 57 65 mpbid ⊢ ( ( ( 𝜑 ∧ ( ( 1 ... ( 𝑁 + 1 ) ) ≈ 𝑠 ∧ 𝑠 ⊆ 𝐴 ) ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑠 ) ) , 𝑠 ) ) → 𝑓 : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ 𝑠 )
67 f1of1 ⊢ ( 𝑓 : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ 𝑠 → 𝑓 : ( 1 ... ( 𝑁 + 1 ) ) –1-1→ 𝑠 )
68 66 67 syl ⊢ ( ( ( 𝜑 ∧ ( ( 1 ... ( 𝑁 + 1 ) ) ≈ 𝑠 ∧ 𝑠 ⊆ 𝐴 ) ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑠 ) ) , 𝑠 ) ) → 𝑓 : ( 1 ... ( 𝑁 + 1 ) ) –1-1→ 𝑠 )
69 simplrr ⊢ ( ( ( 𝜑 ∧ ( ( 1 ... ( 𝑁 + 1 ) ) ≈ 𝑠 ∧ 𝑠 ⊆ 𝐴 ) ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑠 ) ) , 𝑠 ) ) → 𝑠 ⊆ 𝐴 )
70 f1ss ⊢ ( ( 𝑓 : ( 1 ... ( 𝑁 + 1 ) ) –1-1→ 𝑠 ∧ 𝑠 ⊆ 𝐴 ) → 𝑓 : ( 1 ... ( 𝑁 + 1 ) ) –1-1→ 𝐴 )
71 68 69 70 syl2anc ⊢ ( ( ( 𝜑 ∧ ( ( 1 ... ( 𝑁 + 1 ) ) ≈ 𝑠 ∧ 𝑠 ⊆ 𝐴 ) ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑠 ) ) , 𝑠 ) ) → 𝑓 : ( 1 ... ( 𝑁 + 1 ) ) –1-1→ 𝐴 )
72 simpr ⊢ ( ( ( 𝜑 ∧ ( ( 1 ... ( 𝑁 + 1 ) ) ≈ 𝑠 ∧ 𝑠 ⊆ 𝐴 ) ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑠 ) ) , 𝑠 ) ) → 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑠 ) ) , 𝑠 ) )
73 f1ofo ⊢ ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑠 ) ) –1-1-onto→ 𝑠 → 𝑓 : ( 1 ... ( ♯ ‘ 𝑠 ) ) –onto→ 𝑠 )
74 forn ⊢ ( 𝑓 : ( 1 ... ( ♯ ‘ 𝑠 ) ) –onto→ 𝑠 → ran 𝑓 = 𝑠 )
75 isoeq5 ⊢ ( ran 𝑓 = 𝑠 → ( 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑠 ) ) , ran 𝑓 ) ↔ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑠 ) ) , 𝑠 ) ) )
76 57 73 74 75 4syl ⊢ ( ( ( 𝜑 ∧ ( ( 1 ... ( 𝑁 + 1 ) ) ≈ 𝑠 ∧ 𝑠 ⊆ 𝐴 ) ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑠 ) ) , 𝑠 ) ) → ( 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑠 ) ) , ran 𝑓 ) ↔ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑠 ) ) , 𝑠 ) ) )
77 72 76 mpbird ⊢ ( ( ( 𝜑 ∧ ( ( 1 ... ( 𝑁 + 1 ) ) ≈ 𝑠 ∧ 𝑠 ⊆ 𝐴 ) ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑠 ) ) , 𝑠 ) ) → 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑠 ) ) , ran 𝑓 ) )
78 isoeq4 ⊢ ( ( 1 ... ( ♯ ‘ 𝑠 ) ) = ( 1 ... ( 𝑁 + 1 ) ) → ( 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑠 ) ) , ran 𝑓 ) ↔ 𝑓 Isom < , < ( ( 1 ... ( 𝑁 + 1 ) ) , ran 𝑓 ) ) )
79 64 78 syl ⊢ ( ( ( 𝜑 ∧ ( ( 1 ... ( 𝑁 + 1 ) ) ≈ 𝑠 ∧ 𝑠 ⊆ 𝐴 ) ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑠 ) ) , 𝑠 ) ) → ( 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑠 ) ) , ran 𝑓 ) ↔ 𝑓 Isom < , < ( ( 1 ... ( 𝑁 + 1 ) ) , ran 𝑓 ) ) )
80 77 79 mpbid ⊢ ( ( ( 𝜑 ∧ ( ( 1 ... ( 𝑁 + 1 ) ) ≈ 𝑠 ∧ 𝑠 ⊆ 𝐴 ) ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑠 ) ) , 𝑠 ) ) → 𝑓 Isom < , < ( ( 1 ... ( 𝑁 + 1 ) ) , ran 𝑓 ) )
81 71 80 jca ⊢ ( ( ( 𝜑 ∧ ( ( 1 ... ( 𝑁 + 1 ) ) ≈ 𝑠 ∧ 𝑠 ⊆ 𝐴 ) ) ∧ 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑠 ) ) , 𝑠 ) ) → ( 𝑓 : ( 1 ... ( 𝑁 + 1 ) ) –1-1→ 𝐴 ∧ 𝑓 Isom < , < ( ( 1 ... ( 𝑁 + 1 ) ) , ran 𝑓 ) ) )
82 81 ex ⊢ ( ( 𝜑 ∧ ( ( 1 ... ( 𝑁 + 1 ) ) ≈ 𝑠 ∧ 𝑠 ⊆ 𝐴 ) ) → ( 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑠 ) ) , 𝑠 ) → ( 𝑓 : ( 1 ... ( 𝑁 + 1 ) ) –1-1→ 𝐴 ∧ 𝑓 Isom < , < ( ( 1 ... ( 𝑁 + 1 ) ) , ran 𝑓 ) ) ) )
83 82 eximdv ⊢ ( ( 𝜑 ∧ ( ( 1 ... ( 𝑁 + 1 ) ) ≈ 𝑠 ∧ 𝑠 ⊆ 𝐴 ) ) → ( ∃ 𝑓 𝑓 Isom < , < ( ( 1 ... ( ♯ ‘ 𝑠 ) ) , 𝑠 ) → ∃ 𝑓 ( 𝑓 : ( 1 ... ( 𝑁 + 1 ) ) –1-1→ 𝐴 ∧ 𝑓 Isom < , < ( ( 1 ... ( 𝑁 + 1 ) ) , ran 𝑓 ) ) ) )
84 55 83 mpd ⊢ ( ( 𝜑 ∧ ( ( 1 ... ( 𝑁 + 1 ) ) ≈ 𝑠 ∧ 𝑠 ⊆ 𝐴 ) ) → ∃ 𝑓 ( 𝑓 : ( 1 ... ( 𝑁 + 1 ) ) –1-1→ 𝐴 ∧ 𝑓 Isom < , < ( ( 1 ... ( 𝑁 + 1 ) ) , ran 𝑓 ) ) )
85 42 84 exlimddv ⊢ ( 𝜑 → ∃ 𝑓 ( 𝑓 : ( 1 ... ( 𝑁 + 1 ) ) –1-1→ 𝐴 ∧ 𝑓 Isom < , < ( ( 1 ... ( 𝑁 + 1 ) ) , ran 𝑓 ) ) )