Metamath Proof Explorer


Theorem eldioph2lem2

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

Ref Expression
Assertion eldioph2lem2 ( ( ( 𝑁 ∈ ℕ0 ∧ ¬ 𝑆 ∈ Fin ) ∧ ( ( 1 ... 𝑁 ) ⊆ 𝑆𝐴 ∈ ( ℤ𝑁 ) ) ) → ∃ 𝑐 ( 𝑐 : ( 1 ... 𝐴 ) –1-1𝑆 ∧ ( 𝑐 ↾ ( 1 ... 𝑁 ) ) = ( I ↾ ( 1 ... 𝑁 ) ) ) )

Proof

Step Hyp Ref Expression
1 simplr ( ( ( 𝑁 ∈ ℕ0 ∧ ¬ 𝑆 ∈ Fin ) ∧ ( ( 1 ... 𝑁 ) ⊆ 𝑆𝐴 ∈ ( ℤ𝑁 ) ) ) → ¬ 𝑆 ∈ Fin )
2 fzfi ( 1 ... 𝑁 ) ∈ Fin
3 difinf ( ( ¬ 𝑆 ∈ Fin ∧ ( 1 ... 𝑁 ) ∈ Fin ) → ¬ ( 𝑆 ∖ ( 1 ... 𝑁 ) ) ∈ Fin )
4 1 2 3 sylancl ( ( ( 𝑁 ∈ ℕ0 ∧ ¬ 𝑆 ∈ Fin ) ∧ ( ( 1 ... 𝑁 ) ⊆ 𝑆𝐴 ∈ ( ℤ𝑁 ) ) ) → ¬ ( 𝑆 ∖ ( 1 ... 𝑁 ) ) ∈ Fin )
5 fzfi ( 1 ... 𝐴 ) ∈ Fin
6 diffi ( ( 1 ... 𝐴 ) ∈ Fin → ( ( 1 ... 𝐴 ) ∖ ( 1 ... 𝑁 ) ) ∈ Fin )
7 5 6 ax-mp ( ( 1 ... 𝐴 ) ∖ ( 1 ... 𝑁 ) ) ∈ Fin
8 isinffi ( ( ¬ ( 𝑆 ∖ ( 1 ... 𝑁 ) ) ∈ Fin ∧ ( ( 1 ... 𝐴 ) ∖ ( 1 ... 𝑁 ) ) ∈ Fin ) → ∃ 𝑎 𝑎 : ( ( 1 ... 𝐴 ) ∖ ( 1 ... 𝑁 ) ) –1-1→ ( 𝑆 ∖ ( 1 ... 𝑁 ) ) )
9 4 7 8 sylancl ( ( ( 𝑁 ∈ ℕ0 ∧ ¬ 𝑆 ∈ Fin ) ∧ ( ( 1 ... 𝑁 ) ⊆ 𝑆𝐴 ∈ ( ℤ𝑁 ) ) ) → ∃ 𝑎 𝑎 : ( ( 1 ... 𝐴 ) ∖ ( 1 ... 𝑁 ) ) –1-1→ ( 𝑆 ∖ ( 1 ... 𝑁 ) ) )
10 f1f1orn ( 𝑎 : ( ( 1 ... 𝐴 ) ∖ ( 1 ... 𝑁 ) ) –1-1→ ( 𝑆 ∖ ( 1 ... 𝑁 ) ) → 𝑎 : ( ( 1 ... 𝐴 ) ∖ ( 1 ... 𝑁 ) ) –1-1-onto→ ran 𝑎 )
11 10 adantl ( ( ( ( 𝑁 ∈ ℕ0 ∧ ¬ 𝑆 ∈ Fin ) ∧ ( ( 1 ... 𝑁 ) ⊆ 𝑆𝐴 ∈ ( ℤ𝑁 ) ) ) ∧ 𝑎 : ( ( 1 ... 𝐴 ) ∖ ( 1 ... 𝑁 ) ) –1-1→ ( 𝑆 ∖ ( 1 ... 𝑁 ) ) ) → 𝑎 : ( ( 1 ... 𝐴 ) ∖ ( 1 ... 𝑁 ) ) –1-1-onto→ ran 𝑎 )
12 f1oi ( I ↾ ( 1 ... 𝑁 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 )
13 12 a1i ( ( ( ( 𝑁 ∈ ℕ0 ∧ ¬ 𝑆 ∈ Fin ) ∧ ( ( 1 ... 𝑁 ) ⊆ 𝑆𝐴 ∈ ( ℤ𝑁 ) ) ) ∧ 𝑎 : ( ( 1 ... 𝐴 ) ∖ ( 1 ... 𝑁 ) ) –1-1→ ( 𝑆 ∖ ( 1 ... 𝑁 ) ) ) → ( I ↾ ( 1 ... 𝑁 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) )
14 disjdifr ( ( ( 1 ... 𝐴 ) ∖ ( 1 ... 𝑁 ) ) ∩ ( 1 ... 𝑁 ) ) = ∅
15 14 a1i ( ( ( ( 𝑁 ∈ ℕ0 ∧ ¬ 𝑆 ∈ Fin ) ∧ ( ( 1 ... 𝑁 ) ⊆ 𝑆𝐴 ∈ ( ℤ𝑁 ) ) ) ∧ 𝑎 : ( ( 1 ... 𝐴 ) ∖ ( 1 ... 𝑁 ) ) –1-1→ ( 𝑆 ∖ ( 1 ... 𝑁 ) ) ) → ( ( ( 1 ... 𝐴 ) ∖ ( 1 ... 𝑁 ) ) ∩ ( 1 ... 𝑁 ) ) = ∅ )
16 f1f ( 𝑎 : ( ( 1 ... 𝐴 ) ∖ ( 1 ... 𝑁 ) ) –1-1→ ( 𝑆 ∖ ( 1 ... 𝑁 ) ) → 𝑎 : ( ( 1 ... 𝐴 ) ∖ ( 1 ... 𝑁 ) ) ⟶ ( 𝑆 ∖ ( 1 ... 𝑁 ) ) )
17 16 frnd ( 𝑎 : ( ( 1 ... 𝐴 ) ∖ ( 1 ... 𝑁 ) ) –1-1→ ( 𝑆 ∖ ( 1 ... 𝑁 ) ) → ran 𝑎 ⊆ ( 𝑆 ∖ ( 1 ... 𝑁 ) ) )
18 17 adantl ( ( ( ( 𝑁 ∈ ℕ0 ∧ ¬ 𝑆 ∈ Fin ) ∧ ( ( 1 ... 𝑁 ) ⊆ 𝑆𝐴 ∈ ( ℤ𝑁 ) ) ) ∧ 𝑎 : ( ( 1 ... 𝐴 ) ∖ ( 1 ... 𝑁 ) ) –1-1→ ( 𝑆 ∖ ( 1 ... 𝑁 ) ) ) → ran 𝑎 ⊆ ( 𝑆 ∖ ( 1 ... 𝑁 ) ) )
19 18 ssrind ( ( ( ( 𝑁 ∈ ℕ0 ∧ ¬ 𝑆 ∈ Fin ) ∧ ( ( 1 ... 𝑁 ) ⊆ 𝑆𝐴 ∈ ( ℤ𝑁 ) ) ) ∧ 𝑎 : ( ( 1 ... 𝐴 ) ∖ ( 1 ... 𝑁 ) ) –1-1→ ( 𝑆 ∖ ( 1 ... 𝑁 ) ) ) → ( ran 𝑎 ∩ ( 1 ... 𝑁 ) ) ⊆ ( ( 𝑆 ∖ ( 1 ... 𝑁 ) ) ∩ ( 1 ... 𝑁 ) ) )
20 disjdifr ( ( 𝑆 ∖ ( 1 ... 𝑁 ) ) ∩ ( 1 ... 𝑁 ) ) = ∅
21 19 20 sseqtrdi ( ( ( ( 𝑁 ∈ ℕ0 ∧ ¬ 𝑆 ∈ Fin ) ∧ ( ( 1 ... 𝑁 ) ⊆ 𝑆𝐴 ∈ ( ℤ𝑁 ) ) ) ∧ 𝑎 : ( ( 1 ... 𝐴 ) ∖ ( 1 ... 𝑁 ) ) –1-1→ ( 𝑆 ∖ ( 1 ... 𝑁 ) ) ) → ( ran 𝑎 ∩ ( 1 ... 𝑁 ) ) ⊆ ∅ )
22 ss0 ( ( ran 𝑎 ∩ ( 1 ... 𝑁 ) ) ⊆ ∅ → ( ran 𝑎 ∩ ( 1 ... 𝑁 ) ) = ∅ )
23 21 22 syl ( ( ( ( 𝑁 ∈ ℕ0 ∧ ¬ 𝑆 ∈ Fin ) ∧ ( ( 1 ... 𝑁 ) ⊆ 𝑆𝐴 ∈ ( ℤ𝑁 ) ) ) ∧ 𝑎 : ( ( 1 ... 𝐴 ) ∖ ( 1 ... 𝑁 ) ) –1-1→ ( 𝑆 ∖ ( 1 ... 𝑁 ) ) ) → ( ran 𝑎 ∩ ( 1 ... 𝑁 ) ) = ∅ )
24 f1oun ( ( ( 𝑎 : ( ( 1 ... 𝐴 ) ∖ ( 1 ... 𝑁 ) ) –1-1-onto→ ran 𝑎 ∧ ( I ↾ ( 1 ... 𝑁 ) ) : ( 1 ... 𝑁 ) –1-1-onto→ ( 1 ... 𝑁 ) ) ∧ ( ( ( ( 1 ... 𝐴 ) ∖ ( 1 ... 𝑁 ) ) ∩ ( 1 ... 𝑁 ) ) = ∅ ∧ ( ran 𝑎 ∩ ( 1 ... 𝑁 ) ) = ∅ ) ) → ( 𝑎 ∪ ( I ↾ ( 1 ... 𝑁 ) ) ) : ( ( ( 1 ... 𝐴 ) ∖ ( 1 ... 𝑁 ) ) ∪ ( 1 ... 𝑁 ) ) –1-1-onto→ ( ran 𝑎 ∪ ( 1 ... 𝑁 ) ) )
25 11 13 15 23 24 syl22anc ( ( ( ( 𝑁 ∈ ℕ0 ∧ ¬ 𝑆 ∈ Fin ) ∧ ( ( 1 ... 𝑁 ) ⊆ 𝑆𝐴 ∈ ( ℤ𝑁 ) ) ) ∧ 𝑎 : ( ( 1 ... 𝐴 ) ∖ ( 1 ... 𝑁 ) ) –1-1→ ( 𝑆 ∖ ( 1 ... 𝑁 ) ) ) → ( 𝑎 ∪ ( I ↾ ( 1 ... 𝑁 ) ) ) : ( ( ( 1 ... 𝐴 ) ∖ ( 1 ... 𝑁 ) ) ∪ ( 1 ... 𝑁 ) ) –1-1-onto→ ( ran 𝑎 ∪ ( 1 ... 𝑁 ) ) )
26 f1of1 ( ( 𝑎 ∪ ( I ↾ ( 1 ... 𝑁 ) ) ) : ( ( ( 1 ... 𝐴 ) ∖ ( 1 ... 𝑁 ) ) ∪ ( 1 ... 𝑁 ) ) –1-1-onto→ ( ran 𝑎 ∪ ( 1 ... 𝑁 ) ) → ( 𝑎 ∪ ( I ↾ ( 1 ... 𝑁 ) ) ) : ( ( ( 1 ... 𝐴 ) ∖ ( 1 ... 𝑁 ) ) ∪ ( 1 ... 𝑁 ) ) –1-1→ ( ran 𝑎 ∪ ( 1 ... 𝑁 ) ) )
27 25 26 syl ( ( ( ( 𝑁 ∈ ℕ0 ∧ ¬ 𝑆 ∈ Fin ) ∧ ( ( 1 ... 𝑁 ) ⊆ 𝑆𝐴 ∈ ( ℤ𝑁 ) ) ) ∧ 𝑎 : ( ( 1 ... 𝐴 ) ∖ ( 1 ... 𝑁 ) ) –1-1→ ( 𝑆 ∖ ( 1 ... 𝑁 ) ) ) → ( 𝑎 ∪ ( I ↾ ( 1 ... 𝑁 ) ) ) : ( ( ( 1 ... 𝐴 ) ∖ ( 1 ... 𝑁 ) ) ∪ ( 1 ... 𝑁 ) ) –1-1→ ( ran 𝑎 ∪ ( 1 ... 𝑁 ) ) )
28 uncom ( ( ( 1 ... 𝐴 ) ∖ ( 1 ... 𝑁 ) ) ∪ ( 1 ... 𝑁 ) ) = ( ( 1 ... 𝑁 ) ∪ ( ( 1 ... 𝐴 ) ∖ ( 1 ... 𝑁 ) ) )
29 simplrr ( ( ( ( 𝑁 ∈ ℕ0 ∧ ¬ 𝑆 ∈ Fin ) ∧ ( ( 1 ... 𝑁 ) ⊆ 𝑆𝐴 ∈ ( ℤ𝑁 ) ) ) ∧ 𝑎 : ( ( 1 ... 𝐴 ) ∖ ( 1 ... 𝑁 ) ) –1-1→ ( 𝑆 ∖ ( 1 ... 𝑁 ) ) ) → 𝐴 ∈ ( ℤ𝑁 ) )
30 fzss2 ( 𝐴 ∈ ( ℤ𝑁 ) → ( 1 ... 𝑁 ) ⊆ ( 1 ... 𝐴 ) )
31 29 30 syl ( ( ( ( 𝑁 ∈ ℕ0 ∧ ¬ 𝑆 ∈ Fin ) ∧ ( ( 1 ... 𝑁 ) ⊆ 𝑆𝐴 ∈ ( ℤ𝑁 ) ) ) ∧ 𝑎 : ( ( 1 ... 𝐴 ) ∖ ( 1 ... 𝑁 ) ) –1-1→ ( 𝑆 ∖ ( 1 ... 𝑁 ) ) ) → ( 1 ... 𝑁 ) ⊆ ( 1 ... 𝐴 ) )
32 undif ( ( 1 ... 𝑁 ) ⊆ ( 1 ... 𝐴 ) ↔ ( ( 1 ... 𝑁 ) ∪ ( ( 1 ... 𝐴 ) ∖ ( 1 ... 𝑁 ) ) ) = ( 1 ... 𝐴 ) )
33 31 32 sylib ( ( ( ( 𝑁 ∈ ℕ0 ∧ ¬ 𝑆 ∈ Fin ) ∧ ( ( 1 ... 𝑁 ) ⊆ 𝑆𝐴 ∈ ( ℤ𝑁 ) ) ) ∧ 𝑎 : ( ( 1 ... 𝐴 ) ∖ ( 1 ... 𝑁 ) ) –1-1→ ( 𝑆 ∖ ( 1 ... 𝑁 ) ) ) → ( ( 1 ... 𝑁 ) ∪ ( ( 1 ... 𝐴 ) ∖ ( 1 ... 𝑁 ) ) ) = ( 1 ... 𝐴 ) )
34 28 33 syl5eq ( ( ( ( 𝑁 ∈ ℕ0 ∧ ¬ 𝑆 ∈ Fin ) ∧ ( ( 1 ... 𝑁 ) ⊆ 𝑆𝐴 ∈ ( ℤ𝑁 ) ) ) ∧ 𝑎 : ( ( 1 ... 𝐴 ) ∖ ( 1 ... 𝑁 ) ) –1-1→ ( 𝑆 ∖ ( 1 ... 𝑁 ) ) ) → ( ( ( 1 ... 𝐴 ) ∖ ( 1 ... 𝑁 ) ) ∪ ( 1 ... 𝑁 ) ) = ( 1 ... 𝐴 ) )
35 f1eq2 ( ( ( ( 1 ... 𝐴 ) ∖ ( 1 ... 𝑁 ) ) ∪ ( 1 ... 𝑁 ) ) = ( 1 ... 𝐴 ) → ( ( 𝑎 ∪ ( I ↾ ( 1 ... 𝑁 ) ) ) : ( ( ( 1 ... 𝐴 ) ∖ ( 1 ... 𝑁 ) ) ∪ ( 1 ... 𝑁 ) ) –1-1→ ( ran 𝑎 ∪ ( 1 ... 𝑁 ) ) ↔ ( 𝑎 ∪ ( I ↾ ( 1 ... 𝑁 ) ) ) : ( 1 ... 𝐴 ) –1-1→ ( ran 𝑎 ∪ ( 1 ... 𝑁 ) ) ) )
36 34 35 syl ( ( ( ( 𝑁 ∈ ℕ0 ∧ ¬ 𝑆 ∈ Fin ) ∧ ( ( 1 ... 𝑁 ) ⊆ 𝑆𝐴 ∈ ( ℤ𝑁 ) ) ) ∧ 𝑎 : ( ( 1 ... 𝐴 ) ∖ ( 1 ... 𝑁 ) ) –1-1→ ( 𝑆 ∖ ( 1 ... 𝑁 ) ) ) → ( ( 𝑎 ∪ ( I ↾ ( 1 ... 𝑁 ) ) ) : ( ( ( 1 ... 𝐴 ) ∖ ( 1 ... 𝑁 ) ) ∪ ( 1 ... 𝑁 ) ) –1-1→ ( ran 𝑎 ∪ ( 1 ... 𝑁 ) ) ↔ ( 𝑎 ∪ ( I ↾ ( 1 ... 𝑁 ) ) ) : ( 1 ... 𝐴 ) –1-1→ ( ran 𝑎 ∪ ( 1 ... 𝑁 ) ) ) )
37 27 36 mpbid ( ( ( ( 𝑁 ∈ ℕ0 ∧ ¬ 𝑆 ∈ Fin ) ∧ ( ( 1 ... 𝑁 ) ⊆ 𝑆𝐴 ∈ ( ℤ𝑁 ) ) ) ∧ 𝑎 : ( ( 1 ... 𝐴 ) ∖ ( 1 ... 𝑁 ) ) –1-1→ ( 𝑆 ∖ ( 1 ... 𝑁 ) ) ) → ( 𝑎 ∪ ( I ↾ ( 1 ... 𝑁 ) ) ) : ( 1 ... 𝐴 ) –1-1→ ( ran 𝑎 ∪ ( 1 ... 𝑁 ) ) )
38 17 difss2d ( 𝑎 : ( ( 1 ... 𝐴 ) ∖ ( 1 ... 𝑁 ) ) –1-1→ ( 𝑆 ∖ ( 1 ... 𝑁 ) ) → ran 𝑎𝑆 )
39 38 adantl ( ( ( ( 𝑁 ∈ ℕ0 ∧ ¬ 𝑆 ∈ Fin ) ∧ ( ( 1 ... 𝑁 ) ⊆ 𝑆𝐴 ∈ ( ℤ𝑁 ) ) ) ∧ 𝑎 : ( ( 1 ... 𝐴 ) ∖ ( 1 ... 𝑁 ) ) –1-1→ ( 𝑆 ∖ ( 1 ... 𝑁 ) ) ) → ran 𝑎𝑆 )
40 simplrl ( ( ( ( 𝑁 ∈ ℕ0 ∧ ¬ 𝑆 ∈ Fin ) ∧ ( ( 1 ... 𝑁 ) ⊆ 𝑆𝐴 ∈ ( ℤ𝑁 ) ) ) ∧ 𝑎 : ( ( 1 ... 𝐴 ) ∖ ( 1 ... 𝑁 ) ) –1-1→ ( 𝑆 ∖ ( 1 ... 𝑁 ) ) ) → ( 1 ... 𝑁 ) ⊆ 𝑆 )
41 39 40 unssd ( ( ( ( 𝑁 ∈ ℕ0 ∧ ¬ 𝑆 ∈ Fin ) ∧ ( ( 1 ... 𝑁 ) ⊆ 𝑆𝐴 ∈ ( ℤ𝑁 ) ) ) ∧ 𝑎 : ( ( 1 ... 𝐴 ) ∖ ( 1 ... 𝑁 ) ) –1-1→ ( 𝑆 ∖ ( 1 ... 𝑁 ) ) ) → ( ran 𝑎 ∪ ( 1 ... 𝑁 ) ) ⊆ 𝑆 )
42 f1ss ( ( ( 𝑎 ∪ ( I ↾ ( 1 ... 𝑁 ) ) ) : ( 1 ... 𝐴 ) –1-1→ ( ran 𝑎 ∪ ( 1 ... 𝑁 ) ) ∧ ( ran 𝑎 ∪ ( 1 ... 𝑁 ) ) ⊆ 𝑆 ) → ( 𝑎 ∪ ( I ↾ ( 1 ... 𝑁 ) ) ) : ( 1 ... 𝐴 ) –1-1𝑆 )
43 37 41 42 syl2anc ( ( ( ( 𝑁 ∈ ℕ0 ∧ ¬ 𝑆 ∈ Fin ) ∧ ( ( 1 ... 𝑁 ) ⊆ 𝑆𝐴 ∈ ( ℤ𝑁 ) ) ) ∧ 𝑎 : ( ( 1 ... 𝐴 ) ∖ ( 1 ... 𝑁 ) ) –1-1→ ( 𝑆 ∖ ( 1 ... 𝑁 ) ) ) → ( 𝑎 ∪ ( I ↾ ( 1 ... 𝑁 ) ) ) : ( 1 ... 𝐴 ) –1-1𝑆 )
44 resundir ( ( 𝑎 ∪ ( I ↾ ( 1 ... 𝑁 ) ) ) ↾ ( 1 ... 𝑁 ) ) = ( ( 𝑎 ↾ ( 1 ... 𝑁 ) ) ∪ ( ( I ↾ ( 1 ... 𝑁 ) ) ↾ ( 1 ... 𝑁 ) ) )
45 dmres dom ( 𝑎 ↾ ( 1 ... 𝑁 ) ) = ( ( 1 ... 𝑁 ) ∩ dom 𝑎 )
46 incom ( ( 1 ... 𝑁 ) ∩ dom 𝑎 ) = ( dom 𝑎 ∩ ( 1 ... 𝑁 ) )
47 f1dm ( 𝑎 : ( ( 1 ... 𝐴 ) ∖ ( 1 ... 𝑁 ) ) –1-1→ ( 𝑆 ∖ ( 1 ... 𝑁 ) ) → dom 𝑎 = ( ( 1 ... 𝐴 ) ∖ ( 1 ... 𝑁 ) ) )
48 47 adantl ( ( ( ( 𝑁 ∈ ℕ0 ∧ ¬ 𝑆 ∈ Fin ) ∧ ( ( 1 ... 𝑁 ) ⊆ 𝑆𝐴 ∈ ( ℤ𝑁 ) ) ) ∧ 𝑎 : ( ( 1 ... 𝐴 ) ∖ ( 1 ... 𝑁 ) ) –1-1→ ( 𝑆 ∖ ( 1 ... 𝑁 ) ) ) → dom 𝑎 = ( ( 1 ... 𝐴 ) ∖ ( 1 ... 𝑁 ) ) )
49 48 ineq1d ( ( ( ( 𝑁 ∈ ℕ0 ∧ ¬ 𝑆 ∈ Fin ) ∧ ( ( 1 ... 𝑁 ) ⊆ 𝑆𝐴 ∈ ( ℤ𝑁 ) ) ) ∧ 𝑎 : ( ( 1 ... 𝐴 ) ∖ ( 1 ... 𝑁 ) ) –1-1→ ( 𝑆 ∖ ( 1 ... 𝑁 ) ) ) → ( dom 𝑎 ∩ ( 1 ... 𝑁 ) ) = ( ( ( 1 ... 𝐴 ) ∖ ( 1 ... 𝑁 ) ) ∩ ( 1 ... 𝑁 ) ) )
50 49 14 eqtrdi ( ( ( ( 𝑁 ∈ ℕ0 ∧ ¬ 𝑆 ∈ Fin ) ∧ ( ( 1 ... 𝑁 ) ⊆ 𝑆𝐴 ∈ ( ℤ𝑁 ) ) ) ∧ 𝑎 : ( ( 1 ... 𝐴 ) ∖ ( 1 ... 𝑁 ) ) –1-1→ ( 𝑆 ∖ ( 1 ... 𝑁 ) ) ) → ( dom 𝑎 ∩ ( 1 ... 𝑁 ) ) = ∅ )
51 46 50 syl5eq ( ( ( ( 𝑁 ∈ ℕ0 ∧ ¬ 𝑆 ∈ Fin ) ∧ ( ( 1 ... 𝑁 ) ⊆ 𝑆𝐴 ∈ ( ℤ𝑁 ) ) ) ∧ 𝑎 : ( ( 1 ... 𝐴 ) ∖ ( 1 ... 𝑁 ) ) –1-1→ ( 𝑆 ∖ ( 1 ... 𝑁 ) ) ) → ( ( 1 ... 𝑁 ) ∩ dom 𝑎 ) = ∅ )
52 45 51 syl5eq ( ( ( ( 𝑁 ∈ ℕ0 ∧ ¬ 𝑆 ∈ Fin ) ∧ ( ( 1 ... 𝑁 ) ⊆ 𝑆𝐴 ∈ ( ℤ𝑁 ) ) ) ∧ 𝑎 : ( ( 1 ... 𝐴 ) ∖ ( 1 ... 𝑁 ) ) –1-1→ ( 𝑆 ∖ ( 1 ... 𝑁 ) ) ) → dom ( 𝑎 ↾ ( 1 ... 𝑁 ) ) = ∅ )
53 relres Rel ( 𝑎 ↾ ( 1 ... 𝑁 ) )
54 reldm0 ( Rel ( 𝑎 ↾ ( 1 ... 𝑁 ) ) → ( ( 𝑎 ↾ ( 1 ... 𝑁 ) ) = ∅ ↔ dom ( 𝑎 ↾ ( 1 ... 𝑁 ) ) = ∅ ) )
55 53 54 ax-mp ( ( 𝑎 ↾ ( 1 ... 𝑁 ) ) = ∅ ↔ dom ( 𝑎 ↾ ( 1 ... 𝑁 ) ) = ∅ )
56 52 55 sylibr ( ( ( ( 𝑁 ∈ ℕ0 ∧ ¬ 𝑆 ∈ Fin ) ∧ ( ( 1 ... 𝑁 ) ⊆ 𝑆𝐴 ∈ ( ℤ𝑁 ) ) ) ∧ 𝑎 : ( ( 1 ... 𝐴 ) ∖ ( 1 ... 𝑁 ) ) –1-1→ ( 𝑆 ∖ ( 1 ... 𝑁 ) ) ) → ( 𝑎 ↾ ( 1 ... 𝑁 ) ) = ∅ )
57 residm ( ( I ↾ ( 1 ... 𝑁 ) ) ↾ ( 1 ... 𝑁 ) ) = ( I ↾ ( 1 ... 𝑁 ) )
58 57 a1i ( ( ( ( 𝑁 ∈ ℕ0 ∧ ¬ 𝑆 ∈ Fin ) ∧ ( ( 1 ... 𝑁 ) ⊆ 𝑆𝐴 ∈ ( ℤ𝑁 ) ) ) ∧ 𝑎 : ( ( 1 ... 𝐴 ) ∖ ( 1 ... 𝑁 ) ) –1-1→ ( 𝑆 ∖ ( 1 ... 𝑁 ) ) ) → ( ( I ↾ ( 1 ... 𝑁 ) ) ↾ ( 1 ... 𝑁 ) ) = ( I ↾ ( 1 ... 𝑁 ) ) )
59 56 58 uneq12d ( ( ( ( 𝑁 ∈ ℕ0 ∧ ¬ 𝑆 ∈ Fin ) ∧ ( ( 1 ... 𝑁 ) ⊆ 𝑆𝐴 ∈ ( ℤ𝑁 ) ) ) ∧ 𝑎 : ( ( 1 ... 𝐴 ) ∖ ( 1 ... 𝑁 ) ) –1-1→ ( 𝑆 ∖ ( 1 ... 𝑁 ) ) ) → ( ( 𝑎 ↾ ( 1 ... 𝑁 ) ) ∪ ( ( I ↾ ( 1 ... 𝑁 ) ) ↾ ( 1 ... 𝑁 ) ) ) = ( ∅ ∪ ( I ↾ ( 1 ... 𝑁 ) ) ) )
60 uncom ( ∅ ∪ ( I ↾ ( 1 ... 𝑁 ) ) ) = ( ( I ↾ ( 1 ... 𝑁 ) ) ∪ ∅ )
61 un0 ( ( I ↾ ( 1 ... 𝑁 ) ) ∪ ∅ ) = ( I ↾ ( 1 ... 𝑁 ) )
62 60 61 eqtri ( ∅ ∪ ( I ↾ ( 1 ... 𝑁 ) ) ) = ( I ↾ ( 1 ... 𝑁 ) )
63 59 62 eqtrdi ( ( ( ( 𝑁 ∈ ℕ0 ∧ ¬ 𝑆 ∈ Fin ) ∧ ( ( 1 ... 𝑁 ) ⊆ 𝑆𝐴 ∈ ( ℤ𝑁 ) ) ) ∧ 𝑎 : ( ( 1 ... 𝐴 ) ∖ ( 1 ... 𝑁 ) ) –1-1→ ( 𝑆 ∖ ( 1 ... 𝑁 ) ) ) → ( ( 𝑎 ↾ ( 1 ... 𝑁 ) ) ∪ ( ( I ↾ ( 1 ... 𝑁 ) ) ↾ ( 1 ... 𝑁 ) ) ) = ( I ↾ ( 1 ... 𝑁 ) ) )
64 44 63 syl5eq ( ( ( ( 𝑁 ∈ ℕ0 ∧ ¬ 𝑆 ∈ Fin ) ∧ ( ( 1 ... 𝑁 ) ⊆ 𝑆𝐴 ∈ ( ℤ𝑁 ) ) ) ∧ 𝑎 : ( ( 1 ... 𝐴 ) ∖ ( 1 ... 𝑁 ) ) –1-1→ ( 𝑆 ∖ ( 1 ... 𝑁 ) ) ) → ( ( 𝑎 ∪ ( I ↾ ( 1 ... 𝑁 ) ) ) ↾ ( 1 ... 𝑁 ) ) = ( I ↾ ( 1 ... 𝑁 ) ) )
65 vex 𝑎 ∈ V
66 ovex ( 1 ... 𝑁 ) ∈ V
67 resiexg ( ( 1 ... 𝑁 ) ∈ V → ( I ↾ ( 1 ... 𝑁 ) ) ∈ V )
68 66 67 ax-mp ( I ↾ ( 1 ... 𝑁 ) ) ∈ V
69 65 68 unex ( 𝑎 ∪ ( I ↾ ( 1 ... 𝑁 ) ) ) ∈ V
70 f1eq1 ( 𝑐 = ( 𝑎 ∪ ( I ↾ ( 1 ... 𝑁 ) ) ) → ( 𝑐 : ( 1 ... 𝐴 ) –1-1𝑆 ↔ ( 𝑎 ∪ ( I ↾ ( 1 ... 𝑁 ) ) ) : ( 1 ... 𝐴 ) –1-1𝑆 ) )
71 reseq1 ( 𝑐 = ( 𝑎 ∪ ( I ↾ ( 1 ... 𝑁 ) ) ) → ( 𝑐 ↾ ( 1 ... 𝑁 ) ) = ( ( 𝑎 ∪ ( I ↾ ( 1 ... 𝑁 ) ) ) ↾ ( 1 ... 𝑁 ) ) )
72 71 eqeq1d ( 𝑐 = ( 𝑎 ∪ ( I ↾ ( 1 ... 𝑁 ) ) ) → ( ( 𝑐 ↾ ( 1 ... 𝑁 ) ) = ( I ↾ ( 1 ... 𝑁 ) ) ↔ ( ( 𝑎 ∪ ( I ↾ ( 1 ... 𝑁 ) ) ) ↾ ( 1 ... 𝑁 ) ) = ( I ↾ ( 1 ... 𝑁 ) ) ) )
73 70 72 anbi12d ( 𝑐 = ( 𝑎 ∪ ( I ↾ ( 1 ... 𝑁 ) ) ) → ( ( 𝑐 : ( 1 ... 𝐴 ) –1-1𝑆 ∧ ( 𝑐 ↾ ( 1 ... 𝑁 ) ) = ( I ↾ ( 1 ... 𝑁 ) ) ) ↔ ( ( 𝑎 ∪ ( I ↾ ( 1 ... 𝑁 ) ) ) : ( 1 ... 𝐴 ) –1-1𝑆 ∧ ( ( 𝑎 ∪ ( I ↾ ( 1 ... 𝑁 ) ) ) ↾ ( 1 ... 𝑁 ) ) = ( I ↾ ( 1 ... 𝑁 ) ) ) ) )
74 69 73 spcev ( ( ( 𝑎 ∪ ( I ↾ ( 1 ... 𝑁 ) ) ) : ( 1 ... 𝐴 ) –1-1𝑆 ∧ ( ( 𝑎 ∪ ( I ↾ ( 1 ... 𝑁 ) ) ) ↾ ( 1 ... 𝑁 ) ) = ( I ↾ ( 1 ... 𝑁 ) ) ) → ∃ 𝑐 ( 𝑐 : ( 1 ... 𝐴 ) –1-1𝑆 ∧ ( 𝑐 ↾ ( 1 ... 𝑁 ) ) = ( I ↾ ( 1 ... 𝑁 ) ) ) )
75 43 64 74 syl2anc ( ( ( ( 𝑁 ∈ ℕ0 ∧ ¬ 𝑆 ∈ Fin ) ∧ ( ( 1 ... 𝑁 ) ⊆ 𝑆𝐴 ∈ ( ℤ𝑁 ) ) ) ∧ 𝑎 : ( ( 1 ... 𝐴 ) ∖ ( 1 ... 𝑁 ) ) –1-1→ ( 𝑆 ∖ ( 1 ... 𝑁 ) ) ) → ∃ 𝑐 ( 𝑐 : ( 1 ... 𝐴 ) –1-1𝑆 ∧ ( 𝑐 ↾ ( 1 ... 𝑁 ) ) = ( I ↾ ( 1 ... 𝑁 ) ) ) )
76 9 75 exlimddv ( ( ( 𝑁 ∈ ℕ0 ∧ ¬ 𝑆 ∈ Fin ) ∧ ( ( 1 ... 𝑁 ) ⊆ 𝑆𝐴 ∈ ( ℤ𝑁 ) ) ) → ∃ 𝑐 ( 𝑐 : ( 1 ... 𝐴 ) –1-1𝑆 ∧ ( 𝑐 ↾ ( 1 ... 𝑁 ) ) = ( I ↾ ( 1 ... 𝑁 ) ) ) )