Metamath Proof Explorer


Theorem eldioph2lem1

Description: Lemma for eldioph2 . Construct necessary renaming function for one direction. (Contributed by Stefan O'Rear, 8-Oct-2014)

Ref Expression
Assertion eldioph2lem1 ( ( 𝑁 ∈ ℕ0𝐴 ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ 𝐴 ) → ∃ 𝑑 ∈ ( ℤ𝑁 ) ∃ 𝑒 ∈ V ( 𝑒 : ( 1 ... 𝑑 ) –1-1-onto𝐴 ∧ ( 𝑒 ↾ ( 1 ... 𝑁 ) ) = ( I ↾ ( 1 ... 𝑁 ) ) ) )

Proof

Step Hyp Ref Expression
1 nn0re ( 𝑁 ∈ ℕ0𝑁 ∈ ℝ )
2 1 3ad2ant1 ( ( 𝑁 ∈ ℕ0𝐴 ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ 𝐴 ) → 𝑁 ∈ ℝ )
3 2 recnd ( ( 𝑁 ∈ ℕ0𝐴 ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ 𝐴 ) → 𝑁 ∈ ℂ )
4 ax-1cn 1 ∈ ℂ
5 addcom ( ( 𝑁 ∈ ℂ ∧ 1 ∈ ℂ ) → ( 𝑁 + 1 ) = ( 1 + 𝑁 ) )
6 3 4 5 sylancl ( ( 𝑁 ∈ ℕ0𝐴 ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ 𝐴 ) → ( 𝑁 + 1 ) = ( 1 + 𝑁 ) )
7 diffi ( 𝐴 ∈ Fin → ( 𝐴 ∖ ( 1 ... 𝑁 ) ) ∈ Fin )
8 7 3ad2ant2 ( ( 𝑁 ∈ ℕ0𝐴 ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ 𝐴 ) → ( 𝐴 ∖ ( 1 ... 𝑁 ) ) ∈ Fin )
9 fzfid ( ( 𝑁 ∈ ℕ0𝐴 ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ 𝐴 ) → ( 1 ... 𝑁 ) ∈ Fin )
10 disjdifr ( ( 𝐴 ∖ ( 1 ... 𝑁 ) ) ∩ ( 1 ... 𝑁 ) ) = ∅
11 10 a1i ( ( 𝑁 ∈ ℕ0𝐴 ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ 𝐴 ) → ( ( 𝐴 ∖ ( 1 ... 𝑁 ) ) ∩ ( 1 ... 𝑁 ) ) = ∅ )
12 hashun ( ( ( 𝐴 ∖ ( 1 ... 𝑁 ) ) ∈ Fin ∧ ( 1 ... 𝑁 ) ∈ Fin ∧ ( ( 𝐴 ∖ ( 1 ... 𝑁 ) ) ∩ ( 1 ... 𝑁 ) ) = ∅ ) → ( ♯ ‘ ( ( 𝐴 ∖ ( 1 ... 𝑁 ) ) ∪ ( 1 ... 𝑁 ) ) ) = ( ( ♯ ‘ ( 𝐴 ∖ ( 1 ... 𝑁 ) ) ) + ( ♯ ‘ ( 1 ... 𝑁 ) ) ) )
13 8 9 11 12 syl3anc ( ( 𝑁 ∈ ℕ0𝐴 ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ 𝐴 ) → ( ♯ ‘ ( ( 𝐴 ∖ ( 1 ... 𝑁 ) ) ∪ ( 1 ... 𝑁 ) ) ) = ( ( ♯ ‘ ( 𝐴 ∖ ( 1 ... 𝑁 ) ) ) + ( ♯ ‘ ( 1 ... 𝑁 ) ) ) )
14 uncom ( ( 𝐴 ∖ ( 1 ... 𝑁 ) ) ∪ ( 1 ... 𝑁 ) ) = ( ( 1 ... 𝑁 ) ∪ ( 𝐴 ∖ ( 1 ... 𝑁 ) ) )
15 simp3 ( ( 𝑁 ∈ ℕ0𝐴 ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ 𝐴 ) → ( 1 ... 𝑁 ) ⊆ 𝐴 )
16 undif ( ( 1 ... 𝑁 ) ⊆ 𝐴 ↔ ( ( 1 ... 𝑁 ) ∪ ( 𝐴 ∖ ( 1 ... 𝑁 ) ) ) = 𝐴 )
17 15 16 sylib ( ( 𝑁 ∈ ℕ0𝐴 ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ 𝐴 ) → ( ( 1 ... 𝑁 ) ∪ ( 𝐴 ∖ ( 1 ... 𝑁 ) ) ) = 𝐴 )
18 14 17 syl5eq ( ( 𝑁 ∈ ℕ0𝐴 ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ 𝐴 ) → ( ( 𝐴 ∖ ( 1 ... 𝑁 ) ) ∪ ( 1 ... 𝑁 ) ) = 𝐴 )
19 18 fveq2d ( ( 𝑁 ∈ ℕ0𝐴 ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ 𝐴 ) → ( ♯ ‘ ( ( 𝐴 ∖ ( 1 ... 𝑁 ) ) ∪ ( 1 ... 𝑁 ) ) ) = ( ♯ ‘ 𝐴 ) )
20 hashfz1 ( 𝑁 ∈ ℕ0 → ( ♯ ‘ ( 1 ... 𝑁 ) ) = 𝑁 )
21 20 3ad2ant1 ( ( 𝑁 ∈ ℕ0𝐴 ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ 𝐴 ) → ( ♯ ‘ ( 1 ... 𝑁 ) ) = 𝑁 )
22 21 oveq2d ( ( 𝑁 ∈ ℕ0𝐴 ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ 𝐴 ) → ( ( ♯ ‘ ( 𝐴 ∖ ( 1 ... 𝑁 ) ) ) + ( ♯ ‘ ( 1 ... 𝑁 ) ) ) = ( ( ♯ ‘ ( 𝐴 ∖ ( 1 ... 𝑁 ) ) ) + 𝑁 ) )
23 13 19 22 3eqtr3d ( ( 𝑁 ∈ ℕ0𝐴 ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ 𝐴 ) → ( ♯ ‘ 𝐴 ) = ( ( ♯ ‘ ( 𝐴 ∖ ( 1 ... 𝑁 ) ) ) + 𝑁 ) )
24 6 23 oveq12d ( ( 𝑁 ∈ ℕ0𝐴 ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ 𝐴 ) → ( ( 𝑁 + 1 ) ... ( ♯ ‘ 𝐴 ) ) = ( ( 1 + 𝑁 ) ... ( ( ♯ ‘ ( 𝐴 ∖ ( 1 ... 𝑁 ) ) ) + 𝑁 ) ) )
25 24 fveq2d ( ( 𝑁 ∈ ℕ0𝐴 ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ 𝐴 ) → ( ♯ ‘ ( ( 𝑁 + 1 ) ... ( ♯ ‘ 𝐴 ) ) ) = ( ♯ ‘ ( ( 1 + 𝑁 ) ... ( ( ♯ ‘ ( 𝐴 ∖ ( 1 ... 𝑁 ) ) ) + 𝑁 ) ) ) )
26 1zzd ( ( 𝑁 ∈ ℕ0𝐴 ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ 𝐴 ) → 1 ∈ ℤ )
27 hashcl ( ( 𝐴 ∖ ( 1 ... 𝑁 ) ) ∈ Fin → ( ♯ ‘ ( 𝐴 ∖ ( 1 ... 𝑁 ) ) ) ∈ ℕ0 )
28 8 27 syl ( ( 𝑁 ∈ ℕ0𝐴 ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ 𝐴 ) → ( ♯ ‘ ( 𝐴 ∖ ( 1 ... 𝑁 ) ) ) ∈ ℕ0 )
29 28 nn0zd ( ( 𝑁 ∈ ℕ0𝐴 ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ 𝐴 ) → ( ♯ ‘ ( 𝐴 ∖ ( 1 ... 𝑁 ) ) ) ∈ ℤ )
30 nn0z ( 𝑁 ∈ ℕ0𝑁 ∈ ℤ )
31 30 3ad2ant1 ( ( 𝑁 ∈ ℕ0𝐴 ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ 𝐴 ) → 𝑁 ∈ ℤ )
32 fzen ( ( 1 ∈ ℤ ∧ ( ♯ ‘ ( 𝐴 ∖ ( 1 ... 𝑁 ) ) ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 1 ... ( ♯ ‘ ( 𝐴 ∖ ( 1 ... 𝑁 ) ) ) ) ≈ ( ( 1 + 𝑁 ) ... ( ( ♯ ‘ ( 𝐴 ∖ ( 1 ... 𝑁 ) ) ) + 𝑁 ) ) )
33 26 29 31 32 syl3anc ( ( 𝑁 ∈ ℕ0𝐴 ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ 𝐴 ) → ( 1 ... ( ♯ ‘ ( 𝐴 ∖ ( 1 ... 𝑁 ) ) ) ) ≈ ( ( 1 + 𝑁 ) ... ( ( ♯ ‘ ( 𝐴 ∖ ( 1 ... 𝑁 ) ) ) + 𝑁 ) ) )
34 33 ensymd ( ( 𝑁 ∈ ℕ0𝐴 ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ 𝐴 ) → ( ( 1 + 𝑁 ) ... ( ( ♯ ‘ ( 𝐴 ∖ ( 1 ... 𝑁 ) ) ) + 𝑁 ) ) ≈ ( 1 ... ( ♯ ‘ ( 𝐴 ∖ ( 1 ... 𝑁 ) ) ) ) )
35 fzfi ( ( 1 + 𝑁 ) ... ( ( ♯ ‘ ( 𝐴 ∖ ( 1 ... 𝑁 ) ) ) + 𝑁 ) ) ∈ Fin
36 fzfi ( 1 ... ( ♯ ‘ ( 𝐴 ∖ ( 1 ... 𝑁 ) ) ) ) ∈ Fin
37 hashen ( ( ( ( 1 + 𝑁 ) ... ( ( ♯ ‘ ( 𝐴 ∖ ( 1 ... 𝑁 ) ) ) + 𝑁 ) ) ∈ Fin ∧ ( 1 ... ( ♯ ‘ ( 𝐴 ∖ ( 1 ... 𝑁 ) ) ) ) ∈ Fin ) → ( ( ♯ ‘ ( ( 1 + 𝑁 ) ... ( ( ♯ ‘ ( 𝐴 ∖ ( 1 ... 𝑁 ) ) ) + 𝑁 ) ) ) = ( ♯ ‘ ( 1 ... ( ♯ ‘ ( 𝐴 ∖ ( 1 ... 𝑁 ) ) ) ) ) ↔ ( ( 1 + 𝑁 ) ... ( ( ♯ ‘ ( 𝐴 ∖ ( 1 ... 𝑁 ) ) ) + 𝑁 ) ) ≈ ( 1 ... ( ♯ ‘ ( 𝐴 ∖ ( 1 ... 𝑁 ) ) ) ) ) )
38 35 36 37 mp2an ( ( ♯ ‘ ( ( 1 + 𝑁 ) ... ( ( ♯ ‘ ( 𝐴 ∖ ( 1 ... 𝑁 ) ) ) + 𝑁 ) ) ) = ( ♯ ‘ ( 1 ... ( ♯ ‘ ( 𝐴 ∖ ( 1 ... 𝑁 ) ) ) ) ) ↔ ( ( 1 + 𝑁 ) ... ( ( ♯ ‘ ( 𝐴 ∖ ( 1 ... 𝑁 ) ) ) + 𝑁 ) ) ≈ ( 1 ... ( ♯ ‘ ( 𝐴 ∖ ( 1 ... 𝑁 ) ) ) ) )
39 34 38 sylibr ( ( 𝑁 ∈ ℕ0𝐴 ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ 𝐴 ) → ( ♯ ‘ ( ( 1 + 𝑁 ) ... ( ( ♯ ‘ ( 𝐴 ∖ ( 1 ... 𝑁 ) ) ) + 𝑁 ) ) ) = ( ♯ ‘ ( 1 ... ( ♯ ‘ ( 𝐴 ∖ ( 1 ... 𝑁 ) ) ) ) ) )
40 hashfz1 ( ( ♯ ‘ ( 𝐴 ∖ ( 1 ... 𝑁 ) ) ) ∈ ℕ0 → ( ♯ ‘ ( 1 ... ( ♯ ‘ ( 𝐴 ∖ ( 1 ... 𝑁 ) ) ) ) ) = ( ♯ ‘ ( 𝐴 ∖ ( 1 ... 𝑁 ) ) ) )
41 28 40 syl ( ( 𝑁 ∈ ℕ0𝐴 ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ 𝐴 ) → ( ♯ ‘ ( 1 ... ( ♯ ‘ ( 𝐴 ∖ ( 1 ... 𝑁 ) ) ) ) ) = ( ♯ ‘ ( 𝐴 ∖ ( 1 ... 𝑁 ) ) ) )
42 25 39 41 3eqtrd ( ( 𝑁 ∈ ℕ0𝐴 ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ 𝐴 ) → ( ♯ ‘ ( ( 𝑁 + 1 ) ... ( ♯ ‘ 𝐴 ) ) ) = ( ♯ ‘ ( 𝐴 ∖ ( 1 ... 𝑁 ) ) ) )
43 fzfi ( ( 𝑁 + 1 ) ... ( ♯ ‘ 𝐴 ) ) ∈ Fin
44 hashen ( ( ( ( 𝑁 + 1 ) ... ( ♯ ‘ 𝐴 ) ) ∈ Fin ∧ ( 𝐴 ∖ ( 1 ... 𝑁 ) ) ∈ Fin ) → ( ( ♯ ‘ ( ( 𝑁 + 1 ) ... ( ♯ ‘ 𝐴 ) ) ) = ( ♯ ‘ ( 𝐴 ∖ ( 1 ... 𝑁 ) ) ) ↔ ( ( 𝑁 + 1 ) ... ( ♯ ‘ 𝐴 ) ) ≈ ( 𝐴 ∖ ( 1 ... 𝑁 ) ) ) )
45 43 8 44 sylancr ( ( 𝑁 ∈ ℕ0𝐴 ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ 𝐴 ) → ( ( ♯ ‘ ( ( 𝑁 + 1 ) ... ( ♯ ‘ 𝐴 ) ) ) = ( ♯ ‘ ( 𝐴 ∖ ( 1 ... 𝑁 ) ) ) ↔ ( ( 𝑁 + 1 ) ... ( ♯ ‘ 𝐴 ) ) ≈ ( 𝐴 ∖ ( 1 ... 𝑁 ) ) ) )
46 42 45 mpbid ( ( 𝑁 ∈ ℕ0𝐴 ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ 𝐴 ) → ( ( 𝑁 + 1 ) ... ( ♯ ‘ 𝐴 ) ) ≈ ( 𝐴 ∖ ( 1 ... 𝑁 ) ) )
47 bren ( ( ( 𝑁 + 1 ) ... ( ♯ ‘ 𝐴 ) ) ≈ ( 𝐴 ∖ ( 1 ... 𝑁 ) ) ↔ ∃ 𝑎 𝑎 : ( ( 𝑁 + 1 ) ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ ( 𝐴 ∖ ( 1 ... 𝑁 ) ) )
48 46 47 sylib ( ( 𝑁 ∈ ℕ0𝐴 ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ 𝐴 ) → ∃ 𝑎 𝑎 : ( ( 𝑁 + 1 ) ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ ( 𝐴 ∖ ( 1 ... 𝑁 ) ) )
49 simpl1 ( ( ( 𝑁 ∈ ℕ0𝐴 ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ 𝐴 ) ∧ 𝑎 : ( ( 𝑁 + 1 ) ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ ( 𝐴 ∖ ( 1 ... 𝑁 ) ) ) → 𝑁 ∈ ℕ0 )
50 49 nn0zd ( ( ( 𝑁 ∈ ℕ0𝐴 ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ 𝐴 ) ∧ 𝑎 : ( ( 𝑁 + 1 ) ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ ( 𝐴 ∖ ( 1 ... 𝑁 ) ) ) → 𝑁 ∈ ℤ )
51 simpl2 ( ( ( 𝑁 ∈ ℕ0𝐴 ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ 𝐴 ) ∧ 𝑎 : ( ( 𝑁 + 1 ) ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ ( 𝐴 ∖ ( 1 ... 𝑁 ) ) ) → 𝐴 ∈ Fin )
52 hashcl ( 𝐴 ∈ Fin → ( ♯ ‘ 𝐴 ) ∈ ℕ0 )
53 51 52 syl ( ( ( 𝑁 ∈ ℕ0𝐴 ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ 𝐴 ) ∧ 𝑎 : ( ( 𝑁 + 1 ) ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ ( 𝐴 ∖ ( 1 ... 𝑁 ) ) ) → ( ♯ ‘ 𝐴 ) ∈ ℕ0 )
54 53 nn0zd ( ( ( 𝑁 ∈ ℕ0𝐴 ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ 𝐴 ) ∧ 𝑎 : ( ( 𝑁 + 1 ) ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ ( 𝐴 ∖ ( 1 ... 𝑁 ) ) ) → ( ♯ ‘ 𝐴 ) ∈ ℤ )
55 nn0addge2 ( ( 𝑁 ∈ ℝ ∧ ( ♯ ‘ ( 𝐴 ∖ ( 1 ... 𝑁 ) ) ) ∈ ℕ0 ) → 𝑁 ≤ ( ( ♯ ‘ ( 𝐴 ∖ ( 1 ... 𝑁 ) ) ) + 𝑁 ) )
56 2 28 55 syl2anc ( ( 𝑁 ∈ ℕ0𝐴 ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ 𝐴 ) → 𝑁 ≤ ( ( ♯ ‘ ( 𝐴 ∖ ( 1 ... 𝑁 ) ) ) + 𝑁 ) )
57 56 23 breqtrrd ( ( 𝑁 ∈ ℕ0𝐴 ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ 𝐴 ) → 𝑁 ≤ ( ♯ ‘ 𝐴 ) )
58 57 adantr ( ( ( 𝑁 ∈ ℕ0𝐴 ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ 𝐴 ) ∧ 𝑎 : ( ( 𝑁 + 1 ) ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ ( 𝐴 ∖ ( 1 ... 𝑁 ) ) ) → 𝑁 ≤ ( ♯ ‘ 𝐴 ) )
59 eluz2 ( ( ♯ ‘ 𝐴 ) ∈ ( ℤ𝑁 ) ↔ ( 𝑁 ∈ ℤ ∧ ( ♯ ‘ 𝐴 ) ∈ ℤ ∧ 𝑁 ≤ ( ♯ ‘ 𝐴 ) ) )
60 50 54 58 59 syl3anbrc ( ( ( 𝑁 ∈ ℕ0𝐴 ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ 𝐴 ) ∧ 𝑎 : ( ( 𝑁 + 1 ) ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ ( 𝐴 ∖ ( 1 ... 𝑁 ) ) ) → ( ♯ ‘ 𝐴 ) ∈ ( ℤ𝑁 ) )
61 vex 𝑎 ∈ V
62 ovex ( 1 ... 𝑁 ) ∈ V
63 resiexg ( ( 1 ... 𝑁 ) ∈ V → ( I ↾ ( 1 ... 𝑁 ) ) ∈ V )
64 62 63 ax-mp ( I ↾ ( 1 ... 𝑁 ) ) ∈ V
65 61 64 unex ( 𝑎 ∪ ( I ↾ ( 1 ... 𝑁 ) ) ) ∈ V
66 65 a1i ( ( ( 𝑁 ∈ ℕ0𝐴 ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ 𝐴 ) ∧ 𝑎 : ( ( 𝑁 + 1 ) ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ ( 𝐴 ∖ ( 1 ... 𝑁 ) ) ) → ( 𝑎 ∪ ( I ↾ ( 1 ... 𝑁 ) ) ) ∈ V )
67 simpr ( ( ( 𝑁 ∈ ℕ0𝐴 ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ 𝐴 ) ∧ 𝑎 : ( ( 𝑁 + 1 ) ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ ( 𝐴 ∖ ( 1 ... 𝑁 ) ) ) → 𝑎 : ( ( 𝑁 + 1 ) ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ ( 𝐴 ∖ ( 1 ... 𝑁 ) ) )
68 f1oi ( I ↾ ( 1 ... 𝑁 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 )
69 68 a1i ( ( ( 𝑁 ∈ ℕ0𝐴 ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ 𝐴 ) ∧ 𝑎 : ( ( 𝑁 + 1 ) ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ ( 𝐴 ∖ ( 1 ... 𝑁 ) ) ) → ( I ↾ ( 1 ... 𝑁 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) )
70 incom ( ( ( 𝑁 + 1 ) ... ( ♯ ‘ 𝐴 ) ) ∩ ( 1 ... 𝑁 ) ) = ( ( 1 ... 𝑁 ) ∩ ( ( 𝑁 + 1 ) ... ( ♯ ‘ 𝐴 ) ) )
71 49 nn0red ( ( ( 𝑁 ∈ ℕ0𝐴 ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ 𝐴 ) ∧ 𝑎 : ( ( 𝑁 + 1 ) ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ ( 𝐴 ∖ ( 1 ... 𝑁 ) ) ) → 𝑁 ∈ ℝ )
72 71 ltp1d ( ( ( 𝑁 ∈ ℕ0𝐴 ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ 𝐴 ) ∧ 𝑎 : ( ( 𝑁 + 1 ) ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ ( 𝐴 ∖ ( 1 ... 𝑁 ) ) ) → 𝑁 < ( 𝑁 + 1 ) )
73 fzdisj ( 𝑁 < ( 𝑁 + 1 ) → ( ( 1 ... 𝑁 ) ∩ ( ( 𝑁 + 1 ) ... ( ♯ ‘ 𝐴 ) ) ) = ∅ )
74 72 73 syl ( ( ( 𝑁 ∈ ℕ0𝐴 ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ 𝐴 ) ∧ 𝑎 : ( ( 𝑁 + 1 ) ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ ( 𝐴 ∖ ( 1 ... 𝑁 ) ) ) → ( ( 1 ... 𝑁 ) ∩ ( ( 𝑁 + 1 ) ... ( ♯ ‘ 𝐴 ) ) ) = ∅ )
75 70 74 syl5eq ( ( ( 𝑁 ∈ ℕ0𝐴 ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ 𝐴 ) ∧ 𝑎 : ( ( 𝑁 + 1 ) ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ ( 𝐴 ∖ ( 1 ... 𝑁 ) ) ) → ( ( ( 𝑁 + 1 ) ... ( ♯ ‘ 𝐴 ) ) ∩ ( 1 ... 𝑁 ) ) = ∅ )
76 10 a1i ( ( ( 𝑁 ∈ ℕ0𝐴 ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ 𝐴 ) ∧ 𝑎 : ( ( 𝑁 + 1 ) ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ ( 𝐴 ∖ ( 1 ... 𝑁 ) ) ) → ( ( 𝐴 ∖ ( 1 ... 𝑁 ) ) ∩ ( 1 ... 𝑁 ) ) = ∅ )
77 f1oun ( ( ( 𝑎 : ( ( 𝑁 + 1 ) ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ ( 𝐴 ∖ ( 1 ... 𝑁 ) ) ∧ ( I ↾ ( 1 ... 𝑁 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ) ∧ ( ( ( ( 𝑁 + 1 ) ... ( ♯ ‘ 𝐴 ) ) ∩ ( 1 ... 𝑁 ) ) = ∅ ∧ ( ( 𝐴 ∖ ( 1 ... 𝑁 ) ) ∩ ( 1 ... 𝑁 ) ) = ∅ ) ) → ( 𝑎 ∪ ( I ↾ ( 1 ... 𝑁 ) ) ) : ( ( ( 𝑁 + 1 ) ... ( ♯ ‘ 𝐴 ) ) ∪ ( 1 ... 𝑁 ) ) –1-1-onto→ ( ( 𝐴 ∖ ( 1 ... 𝑁 ) ) ∪ ( 1 ... 𝑁 ) ) )
78 67 69 75 76 77 syl22anc ( ( ( 𝑁 ∈ ℕ0𝐴 ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ 𝐴 ) ∧ 𝑎 : ( ( 𝑁 + 1 ) ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ ( 𝐴 ∖ ( 1 ... 𝑁 ) ) ) → ( 𝑎 ∪ ( I ↾ ( 1 ... 𝑁 ) ) ) : ( ( ( 𝑁 + 1 ) ... ( ♯ ‘ 𝐴 ) ) ∪ ( 1 ... 𝑁 ) ) –1-1-onto→ ( ( 𝐴 ∖ ( 1 ... 𝑁 ) ) ∪ ( 1 ... 𝑁 ) ) )
79 uncom ( ( ( 𝑁 + 1 ) ... ( ♯ ‘ 𝐴 ) ) ∪ ( 1 ... 𝑁 ) ) = ( ( 1 ... 𝑁 ) ∪ ( ( 𝑁 + 1 ) ... ( ♯ ‘ 𝐴 ) ) )
80 fzsplit1nn0 ( ( 𝑁 ∈ ℕ0 ∧ ( ♯ ‘ 𝐴 ) ∈ ℕ0𝑁 ≤ ( ♯ ‘ 𝐴 ) ) → ( 1 ... ( ♯ ‘ 𝐴 ) ) = ( ( 1 ... 𝑁 ) ∪ ( ( 𝑁 + 1 ) ... ( ♯ ‘ 𝐴 ) ) ) )
81 49 53 58 80 syl3anc ( ( ( 𝑁 ∈ ℕ0𝐴 ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ 𝐴 ) ∧ 𝑎 : ( ( 𝑁 + 1 ) ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ ( 𝐴 ∖ ( 1 ... 𝑁 ) ) ) → ( 1 ... ( ♯ ‘ 𝐴 ) ) = ( ( 1 ... 𝑁 ) ∪ ( ( 𝑁 + 1 ) ... ( ♯ ‘ 𝐴 ) ) ) )
82 79 81 eqtr4id ( ( ( 𝑁 ∈ ℕ0𝐴 ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ 𝐴 ) ∧ 𝑎 : ( ( 𝑁 + 1 ) ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ ( 𝐴 ∖ ( 1 ... 𝑁 ) ) ) → ( ( ( 𝑁 + 1 ) ... ( ♯ ‘ 𝐴 ) ) ∪ ( 1 ... 𝑁 ) ) = ( 1 ... ( ♯ ‘ 𝐴 ) ) )
83 simpl3 ( ( ( 𝑁 ∈ ℕ0𝐴 ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ 𝐴 ) ∧ 𝑎 : ( ( 𝑁 + 1 ) ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ ( 𝐴 ∖ ( 1 ... 𝑁 ) ) ) → ( 1 ... 𝑁 ) ⊆ 𝐴 )
84 83 16 sylib ( ( ( 𝑁 ∈ ℕ0𝐴 ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ 𝐴 ) ∧ 𝑎 : ( ( 𝑁 + 1 ) ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ ( 𝐴 ∖ ( 1 ... 𝑁 ) ) ) → ( ( 1 ... 𝑁 ) ∪ ( 𝐴 ∖ ( 1 ... 𝑁 ) ) ) = 𝐴 )
85 14 84 syl5eq ( ( ( 𝑁 ∈ ℕ0𝐴 ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ 𝐴 ) ∧ 𝑎 : ( ( 𝑁 + 1 ) ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ ( 𝐴 ∖ ( 1 ... 𝑁 ) ) ) → ( ( 𝐴 ∖ ( 1 ... 𝑁 ) ) ∪ ( 1 ... 𝑁 ) ) = 𝐴 )
86 f1oeq23 ( ( ( ( ( 𝑁 + 1 ) ... ( ♯ ‘ 𝐴 ) ) ∪ ( 1 ... 𝑁 ) ) = ( 1 ... ( ♯ ‘ 𝐴 ) ) ∧ ( ( 𝐴 ∖ ( 1 ... 𝑁 ) ) ∪ ( 1 ... 𝑁 ) ) = 𝐴 ) → ( ( 𝑎 ∪ ( I ↾ ( 1 ... 𝑁 ) ) ) : ( ( ( 𝑁 + 1 ) ... ( ♯ ‘ 𝐴 ) ) ∪ ( 1 ... 𝑁 ) ) –1-1-onto→ ( ( 𝐴 ∖ ( 1 ... 𝑁 ) ) ∪ ( 1 ... 𝑁 ) ) ↔ ( 𝑎 ∪ ( I ↾ ( 1 ... 𝑁 ) ) ) : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto𝐴 ) )
87 82 85 86 syl2anc ( ( ( 𝑁 ∈ ℕ0𝐴 ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ 𝐴 ) ∧ 𝑎 : ( ( 𝑁 + 1 ) ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ ( 𝐴 ∖ ( 1 ... 𝑁 ) ) ) → ( ( 𝑎 ∪ ( I ↾ ( 1 ... 𝑁 ) ) ) : ( ( ( 𝑁 + 1 ) ... ( ♯ ‘ 𝐴 ) ) ∪ ( 1 ... 𝑁 ) ) –1-1-onto→ ( ( 𝐴 ∖ ( 1 ... 𝑁 ) ) ∪ ( 1 ... 𝑁 ) ) ↔ ( 𝑎 ∪ ( I ↾ ( 1 ... 𝑁 ) ) ) : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto𝐴 ) )
88 78 87 mpbid ( ( ( 𝑁 ∈ ℕ0𝐴 ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ 𝐴 ) ∧ 𝑎 : ( ( 𝑁 + 1 ) ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ ( 𝐴 ∖ ( 1 ... 𝑁 ) ) ) → ( 𝑎 ∪ ( I ↾ ( 1 ... 𝑁 ) ) ) : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto𝐴 )
89 resundir ( ( 𝑎 ∪ ( I ↾ ( 1 ... 𝑁 ) ) ) ↾ ( 1 ... 𝑁 ) ) = ( ( 𝑎 ↾ ( 1 ... 𝑁 ) ) ∪ ( ( I ↾ ( 1 ... 𝑁 ) ) ↾ ( 1 ... 𝑁 ) ) )
90 dmres dom ( 𝑎 ↾ ( 1 ... 𝑁 ) ) = ( ( 1 ... 𝑁 ) ∩ dom 𝑎 )
91 f1odm ( 𝑎 : ( ( 𝑁 + 1 ) ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ ( 𝐴 ∖ ( 1 ... 𝑁 ) ) → dom 𝑎 = ( ( 𝑁 + 1 ) ... ( ♯ ‘ 𝐴 ) ) )
92 91 adantl ( ( ( 𝑁 ∈ ℕ0𝐴 ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ 𝐴 ) ∧ 𝑎 : ( ( 𝑁 + 1 ) ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ ( 𝐴 ∖ ( 1 ... 𝑁 ) ) ) → dom 𝑎 = ( ( 𝑁 + 1 ) ... ( ♯ ‘ 𝐴 ) ) )
93 92 ineq2d ( ( ( 𝑁 ∈ ℕ0𝐴 ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ 𝐴 ) ∧ 𝑎 : ( ( 𝑁 + 1 ) ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ ( 𝐴 ∖ ( 1 ... 𝑁 ) ) ) → ( ( 1 ... 𝑁 ) ∩ dom 𝑎 ) = ( ( 1 ... 𝑁 ) ∩ ( ( 𝑁 + 1 ) ... ( ♯ ‘ 𝐴 ) ) ) )
94 93 74 eqtrd ( ( ( 𝑁 ∈ ℕ0𝐴 ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ 𝐴 ) ∧ 𝑎 : ( ( 𝑁 + 1 ) ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ ( 𝐴 ∖ ( 1 ... 𝑁 ) ) ) → ( ( 1 ... 𝑁 ) ∩ dom 𝑎 ) = ∅ )
95 90 94 syl5eq ( ( ( 𝑁 ∈ ℕ0𝐴 ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ 𝐴 ) ∧ 𝑎 : ( ( 𝑁 + 1 ) ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ ( 𝐴 ∖ ( 1 ... 𝑁 ) ) ) → dom ( 𝑎 ↾ ( 1 ... 𝑁 ) ) = ∅ )
96 relres Rel ( 𝑎 ↾ ( 1 ... 𝑁 ) )
97 reldm0 ( Rel ( 𝑎 ↾ ( 1 ... 𝑁 ) ) → ( ( 𝑎 ↾ ( 1 ... 𝑁 ) ) = ∅ ↔ dom ( 𝑎 ↾ ( 1 ... 𝑁 ) ) = ∅ ) )
98 96 97 ax-mp ( ( 𝑎 ↾ ( 1 ... 𝑁 ) ) = ∅ ↔ dom ( 𝑎 ↾ ( 1 ... 𝑁 ) ) = ∅ )
99 95 98 sylibr ( ( ( 𝑁 ∈ ℕ0𝐴 ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ 𝐴 ) ∧ 𝑎 : ( ( 𝑁 + 1 ) ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ ( 𝐴 ∖ ( 1 ... 𝑁 ) ) ) → ( 𝑎 ↾ ( 1 ... 𝑁 ) ) = ∅ )
100 residm ( ( I ↾ ( 1 ... 𝑁 ) ) ↾ ( 1 ... 𝑁 ) ) = ( I ↾ ( 1 ... 𝑁 ) )
101 100 a1i ( ( ( 𝑁 ∈ ℕ0𝐴 ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ 𝐴 ) ∧ 𝑎 : ( ( 𝑁 + 1 ) ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ ( 𝐴 ∖ ( 1 ... 𝑁 ) ) ) → ( ( I ↾ ( 1 ... 𝑁 ) ) ↾ ( 1 ... 𝑁 ) ) = ( I ↾ ( 1 ... 𝑁 ) ) )
102 99 101 uneq12d ( ( ( 𝑁 ∈ ℕ0𝐴 ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ 𝐴 ) ∧ 𝑎 : ( ( 𝑁 + 1 ) ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ ( 𝐴 ∖ ( 1 ... 𝑁 ) ) ) → ( ( 𝑎 ↾ ( 1 ... 𝑁 ) ) ∪ ( ( I ↾ ( 1 ... 𝑁 ) ) ↾ ( 1 ... 𝑁 ) ) ) = ( ∅ ∪ ( I ↾ ( 1 ... 𝑁 ) ) ) )
103 uncom ( ∅ ∪ ( I ↾ ( 1 ... 𝑁 ) ) ) = ( ( I ↾ ( 1 ... 𝑁 ) ) ∪ ∅ )
104 un0 ( ( I ↾ ( 1 ... 𝑁 ) ) ∪ ∅ ) = ( I ↾ ( 1 ... 𝑁 ) )
105 103 104 eqtri ( ∅ ∪ ( I ↾ ( 1 ... 𝑁 ) ) ) = ( I ↾ ( 1 ... 𝑁 ) )
106 102 105 eqtrdi ( ( ( 𝑁 ∈ ℕ0𝐴 ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ 𝐴 ) ∧ 𝑎 : ( ( 𝑁 + 1 ) ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ ( 𝐴 ∖ ( 1 ... 𝑁 ) ) ) → ( ( 𝑎 ↾ ( 1 ... 𝑁 ) ) ∪ ( ( I ↾ ( 1 ... 𝑁 ) ) ↾ ( 1 ... 𝑁 ) ) ) = ( I ↾ ( 1 ... 𝑁 ) ) )
107 89 106 syl5eq ( ( ( 𝑁 ∈ ℕ0𝐴 ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ 𝐴 ) ∧ 𝑎 : ( ( 𝑁 + 1 ) ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ ( 𝐴 ∖ ( 1 ... 𝑁 ) ) ) → ( ( 𝑎 ∪ ( I ↾ ( 1 ... 𝑁 ) ) ) ↾ ( 1 ... 𝑁 ) ) = ( I ↾ ( 1 ... 𝑁 ) ) )
108 oveq2 ( 𝑑 = ( ♯ ‘ 𝐴 ) → ( 1 ... 𝑑 ) = ( 1 ... ( ♯ ‘ 𝐴 ) ) )
109 108 f1oeq2d ( 𝑑 = ( ♯ ‘ 𝐴 ) → ( 𝑒 : ( 1 ... 𝑑 ) –1-1-onto𝐴𝑒 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto𝐴 ) )
110 109 anbi1d ( 𝑑 = ( ♯ ‘ 𝐴 ) → ( ( 𝑒 : ( 1 ... 𝑑 ) –1-1-onto𝐴 ∧ ( 𝑒 ↾ ( 1 ... 𝑁 ) ) = ( I ↾ ( 1 ... 𝑁 ) ) ) ↔ ( 𝑒 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto𝐴 ∧ ( 𝑒 ↾ ( 1 ... 𝑁 ) ) = ( I ↾ ( 1 ... 𝑁 ) ) ) ) )
111 f1oeq1 ( 𝑒 = ( 𝑎 ∪ ( I ↾ ( 1 ... 𝑁 ) ) ) → ( 𝑒 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto𝐴 ↔ ( 𝑎 ∪ ( I ↾ ( 1 ... 𝑁 ) ) ) : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto𝐴 ) )
112 reseq1 ( 𝑒 = ( 𝑎 ∪ ( I ↾ ( 1 ... 𝑁 ) ) ) → ( 𝑒 ↾ ( 1 ... 𝑁 ) ) = ( ( 𝑎 ∪ ( I ↾ ( 1 ... 𝑁 ) ) ) ↾ ( 1 ... 𝑁 ) ) )
113 112 eqeq1d ( 𝑒 = ( 𝑎 ∪ ( I ↾ ( 1 ... 𝑁 ) ) ) → ( ( 𝑒 ↾ ( 1 ... 𝑁 ) ) = ( I ↾ ( 1 ... 𝑁 ) ) ↔ ( ( 𝑎 ∪ ( I ↾ ( 1 ... 𝑁 ) ) ) ↾ ( 1 ... 𝑁 ) ) = ( I ↾ ( 1 ... 𝑁 ) ) ) )
114 111 113 anbi12d ( 𝑒 = ( 𝑎 ∪ ( I ↾ ( 1 ... 𝑁 ) ) ) → ( ( 𝑒 : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto𝐴 ∧ ( 𝑒 ↾ ( 1 ... 𝑁 ) ) = ( I ↾ ( 1 ... 𝑁 ) ) ) ↔ ( ( 𝑎 ∪ ( I ↾ ( 1 ... 𝑁 ) ) ) : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto𝐴 ∧ ( ( 𝑎 ∪ ( I ↾ ( 1 ... 𝑁 ) ) ) ↾ ( 1 ... 𝑁 ) ) = ( I ↾ ( 1 ... 𝑁 ) ) ) ) )
115 110 114 rspc2ev ( ( ( ♯ ‘ 𝐴 ) ∈ ( ℤ𝑁 ) ∧ ( 𝑎 ∪ ( I ↾ ( 1 ... 𝑁 ) ) ) ∈ V ∧ ( ( 𝑎 ∪ ( I ↾ ( 1 ... 𝑁 ) ) ) : ( 1 ... ( ♯ ‘ 𝐴 ) ) –1-1-onto𝐴 ∧ ( ( 𝑎 ∪ ( I ↾ ( 1 ... 𝑁 ) ) ) ↾ ( 1 ... 𝑁 ) ) = ( I ↾ ( 1 ... 𝑁 ) ) ) ) → ∃ 𝑑 ∈ ( ℤ𝑁 ) ∃ 𝑒 ∈ V ( 𝑒 : ( 1 ... 𝑑 ) –1-1-onto𝐴 ∧ ( 𝑒 ↾ ( 1 ... 𝑁 ) ) = ( I ↾ ( 1 ... 𝑁 ) ) ) )
116 60 66 88 107 115 syl112anc ( ( ( 𝑁 ∈ ℕ0𝐴 ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ 𝐴 ) ∧ 𝑎 : ( ( 𝑁 + 1 ) ... ( ♯ ‘ 𝐴 ) ) –1-1-onto→ ( 𝐴 ∖ ( 1 ... 𝑁 ) ) ) → ∃ 𝑑 ∈ ( ℤ𝑁 ) ∃ 𝑒 ∈ V ( 𝑒 : ( 1 ... 𝑑 ) –1-1-onto𝐴 ∧ ( 𝑒 ↾ ( 1 ... 𝑁 ) ) = ( I ↾ ( 1 ... 𝑁 ) ) ) )
117 48 116 exlimddv ( ( 𝑁 ∈ ℕ0𝐴 ∈ Fin ∧ ( 1 ... 𝑁 ) ⊆ 𝐴 ) → ∃ 𝑑 ∈ ( ℤ𝑁 ) ∃ 𝑒 ∈ V ( 𝑒 : ( 1 ... 𝑑 ) –1-1-onto𝐴 ∧ ( 𝑒 ↾ ( 1 ... 𝑁 ) ) = ( I ↾ ( 1 ... 𝑁 ) ) ) )