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 eqtrid ⊢ ( ( 𝑁 ∈ ℕ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 eqtrid ⊢ ( ( ( 𝑁 ∈ ℕ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 eqtrid ⊢ ( ( ( 𝑁 ∈ ℕ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 eqtrid ⊢ ( ( ( 𝑁 ∈ ℕ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 eqtrid ⊢ ( ( ( 𝑁 ∈ ℕ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 ... 𝑁 ) ) ) )