Theorem eldioph2lem1 37323

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

Assertion

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

Distinct variable groups:   𝐴,𝑑,𝑒   𝑁,𝑑,𝑒

Proof of Theorem eldioph2lem1

Dummy variable 𝑎 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		nn0re 11301	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ)
2	1	3ad2ant1 1082	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ Fin ∧ (1...𝑁) ⊆ 𝐴) → 𝑁 ∈ ℝ)
3	2	recnd 10068	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ Fin ∧ (1...𝑁) ⊆ 𝐴) → 𝑁 ∈ ℂ)
4		ax-1cn 9994	. . . . . . . 8 ⊢ 1 ∈ ℂ
5		addcom 10222	. . . . . . . 8 ⊢ ((𝑁 ∈ ℂ ∧ 1 ∈ ℂ) → (𝑁 + 1) = (1 + 𝑁))
6	3, 4, 5	sylancl 694	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ Fin ∧ (1...𝑁) ⊆ 𝐴) → (𝑁 + 1) = (1 + 𝑁))
7		diffi 8192	. . . . . . . . . 10 ⊢ (𝐴 ∈ Fin → (𝐴 ∖ (1...𝑁)) ∈ Fin)
8	7	3ad2ant2 1083	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ Fin ∧ (1...𝑁) ⊆ 𝐴) → (𝐴 ∖ (1...𝑁)) ∈ Fin)
9		fzfid 12772	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ Fin ∧ (1...𝑁) ⊆ 𝐴) → (1...𝑁) ∈ Fin)
10		incom 3805	. . . . . . . . . . 11 ⊢ ((𝐴 ∖ (1...𝑁)) ∩ (1...𝑁)) = ((1...𝑁) ∩ (𝐴 ∖ (1...𝑁)))
11		disjdif 4040	. . . . . . . . . . 11 ⊢ ((1...𝑁) ∩ (𝐴 ∖ (1...𝑁))) = ∅
12	10, 11	eqtri 2644	. . . . . . . . . 10 ⊢ ((𝐴 ∖ (1...𝑁)) ∩ (1...𝑁)) = ∅
13	12	a1i 11	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ Fin ∧ (1...𝑁) ⊆ 𝐴) → ((𝐴 ∖ (1...𝑁)) ∩ (1...𝑁)) = ∅)
14		hashun 13171	. . . . . . . . 9 ⊢ (((𝐴 ∖ (1...𝑁)) ∈ Fin ∧ (1...𝑁) ∈ Fin ∧ ((𝐴 ∖ (1...𝑁)) ∩ (1...𝑁)) = ∅) → (#‘((𝐴 ∖ (1...𝑁)) ∪ (1...𝑁))) = ((#‘(𝐴 ∖ (1...𝑁))) + (#‘(1...𝑁))))
15	8, 9, 13, 14	syl3anc 1326	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ Fin ∧ (1...𝑁) ⊆ 𝐴) → (#‘((𝐴 ∖ (1...𝑁)) ∪ (1...𝑁))) = ((#‘(𝐴 ∖ (1...𝑁))) + (#‘(1...𝑁))))
16		uncom 3757	. . . . . . . . . 10 ⊢ ((𝐴 ∖ (1...𝑁)) ∪ (1...𝑁)) = ((1...𝑁) ∪ (𝐴 ∖ (1...𝑁)))
17		simp3 1063	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ Fin ∧ (1...𝑁) ⊆ 𝐴) → (1...𝑁) ⊆ 𝐴)
18		undif 4049	. . . . . . . . . . 11 ⊢ ((1...𝑁) ⊆ 𝐴 ↔ ((1...𝑁) ∪ (𝐴 ∖ (1...𝑁))) = 𝐴)
19	17, 18	sylib 208	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ Fin ∧ (1...𝑁) ⊆ 𝐴) → ((1...𝑁) ∪ (𝐴 ∖ (1...𝑁))) = 𝐴)
20	16, 19	syl5eq 2668	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ Fin ∧ (1...𝑁) ⊆ 𝐴) → ((𝐴 ∖ (1...𝑁)) ∪ (1...𝑁)) = 𝐴)
21	20	fveq2d 6195	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ Fin ∧ (1...𝑁) ⊆ 𝐴) → (#‘((𝐴 ∖ (1...𝑁)) ∪ (1...𝑁))) = (#‘𝐴))
22		hashfz1 13134	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ0 → (#‘(1...𝑁)) = 𝑁)
23	22	3ad2ant1 1082	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ Fin ∧ (1...𝑁) ⊆ 𝐴) → (#‘(1...𝑁)) = 𝑁)
24	23	oveq2d 6666	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ Fin ∧ (1...𝑁) ⊆ 𝐴) → ((#‘(𝐴 ∖ (1...𝑁))) + (#‘(1...𝑁))) = ((#‘(𝐴 ∖ (1...𝑁))) + 𝑁))
25	15, 21, 24	3eqtr3d 2664	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ Fin ∧ (1...𝑁) ⊆ 𝐴) → (#‘𝐴) = ((#‘(𝐴 ∖ (1...𝑁))) + 𝑁))
26	6, 25	oveq12d 6668	. . . . . 6 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ Fin ∧ (1...𝑁) ⊆ 𝐴) → ((𝑁 + 1)...(#‘𝐴)) = ((1 + 𝑁)...((#‘(𝐴 ∖ (1...𝑁))) + 𝑁)))
27	26	fveq2d 6195	. . . . 5 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ Fin ∧ (1...𝑁) ⊆ 𝐴) → (#‘((𝑁 + 1)...(#‘𝐴))) = (#‘((1 + 𝑁)...((#‘(𝐴 ∖ (1...𝑁))) + 𝑁))))
28		1zzd 11408	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ Fin ∧ (1...𝑁) ⊆ 𝐴) → 1 ∈ ℤ)
29		hashcl 13147	. . . . . . . . . 10 ⊢ ((𝐴 ∖ (1...𝑁)) ∈ Fin → (#‘(𝐴 ∖ (1...𝑁))) ∈ ℕ0)
30	8, 29	syl 17	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ Fin ∧ (1...𝑁) ⊆ 𝐴) → (#‘(𝐴 ∖ (1...𝑁))) ∈ ℕ0)
31	30	nn0zd 11480	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ Fin ∧ (1...𝑁) ⊆ 𝐴) → (#‘(𝐴 ∖ (1...𝑁))) ∈ ℤ)
32		nn0z 11400	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ)
33	32	3ad2ant1 1082	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ Fin ∧ (1...𝑁) ⊆ 𝐴) → 𝑁 ∈ ℤ)
34		fzen 12358	. . . . . . . 8 ⊢ ((1 ∈ ℤ ∧ (#‘(𝐴 ∖ (1...𝑁))) ∈ ℤ ∧ 𝑁 ∈ ℤ) → (1...(#‘(𝐴 ∖ (1...𝑁)))) ≈ ((1 + 𝑁)...((#‘(𝐴 ∖ (1...𝑁))) + 𝑁)))
35	28, 31, 33, 34	syl3anc 1326	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ Fin ∧ (1...𝑁) ⊆ 𝐴) → (1...(#‘(𝐴 ∖ (1...𝑁)))) ≈ ((1 + 𝑁)...((#‘(𝐴 ∖ (1...𝑁))) + 𝑁)))
36	35	ensymd 8007	. . . . . 6 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ Fin ∧ (1...𝑁) ⊆ 𝐴) → ((1 + 𝑁)...((#‘(𝐴 ∖ (1...𝑁))) + 𝑁)) ≈ (1...(#‘(𝐴 ∖ (1...𝑁)))))
37		fzfi 12771	. . . . . . 7 ⊢ ((1 + 𝑁)...((#‘(𝐴 ∖ (1...𝑁))) + 𝑁)) ∈ Fin
38		fzfi 12771	. . . . . . 7 ⊢ (1...(#‘(𝐴 ∖ (1...𝑁)))) ∈ Fin
39		hashen 13135	. . . . . . 7 ⊢ ((((1 + 𝑁)...((#‘(𝐴 ∖ (1...𝑁))) + 𝑁)) ∈ Fin ∧ (1...(#‘(𝐴 ∖ (1...𝑁)))) ∈ Fin) → ((#‘((1 + 𝑁)...((#‘(𝐴 ∖ (1...𝑁))) + 𝑁))) = (#‘(1...(#‘(𝐴 ∖ (1...𝑁))))) ↔ ((1 + 𝑁)...((#‘(𝐴 ∖ (1...𝑁))) + 𝑁)) ≈ (1...(#‘(𝐴 ∖ (1...𝑁))))))
40	37, 38, 39	mp2an 708	. . . . . 6 ⊢ ((#‘((1 + 𝑁)...((#‘(𝐴 ∖ (1...𝑁))) + 𝑁))) = (#‘(1...(#‘(𝐴 ∖ (1...𝑁))))) ↔ ((1 + 𝑁)...((#‘(𝐴 ∖ (1...𝑁))) + 𝑁)) ≈ (1...(#‘(𝐴 ∖ (1...𝑁)))))
41	36, 40	sylibr 224	. . . . 5 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ Fin ∧ (1...𝑁) ⊆ 𝐴) → (#‘((1 + 𝑁)...((#‘(𝐴 ∖ (1...𝑁))) + 𝑁))) = (#‘(1...(#‘(𝐴 ∖ (1...𝑁))))))
42		hashfz1 13134	. . . . . 6 ⊢ ((#‘(𝐴 ∖ (1...𝑁))) ∈ ℕ0 → (#‘(1...(#‘(𝐴 ∖ (1...𝑁))))) = (#‘(𝐴 ∖ (1...𝑁))))
43	30, 42	syl 17	. . . . 5 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ Fin ∧ (1...𝑁) ⊆ 𝐴) → (#‘(1...(#‘(𝐴 ∖ (1...𝑁))))) = (#‘(𝐴 ∖ (1...𝑁))))
44	27, 41, 43	3eqtrd 2660	. . . 4 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ Fin ∧ (1...𝑁) ⊆ 𝐴) → (#‘((𝑁 + 1)...(#‘𝐴))) = (#‘(𝐴 ∖ (1...𝑁))))
45		fzfi 12771	. . . . 5 ⊢ ((𝑁 + 1)...(#‘𝐴)) ∈ Fin
46		hashen 13135	. . . . 5 ⊢ ((((𝑁 + 1)...(#‘𝐴)) ∈ Fin ∧ (𝐴 ∖ (1...𝑁)) ∈ Fin) → ((#‘((𝑁 + 1)...(#‘𝐴))) = (#‘(𝐴 ∖ (1...𝑁))) ↔ ((𝑁 + 1)...(#‘𝐴)) ≈ (𝐴 ∖ (1...𝑁))))
47	45, 8, 46	sylancr 695	. . . 4 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ Fin ∧ (1...𝑁) ⊆ 𝐴) → ((#‘((𝑁 + 1)...(#‘𝐴))) = (#‘(𝐴 ∖ (1...𝑁))) ↔ ((𝑁 + 1)...(#‘𝐴)) ≈ (𝐴 ∖ (1...𝑁))))
48	44, 47	mpbid 222	. . 3 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ Fin ∧ (1...𝑁) ⊆ 𝐴) → ((𝑁 + 1)...(#‘𝐴)) ≈ (𝐴 ∖ (1...𝑁)))
49		bren 7964	. . 3 ⊢ (((𝑁 + 1)...(#‘𝐴)) ≈ (𝐴 ∖ (1...𝑁)) ↔ ∃𝑎 𝑎:((𝑁 + 1)...(#‘𝐴))–1-1-onto→(𝐴 ∖ (1...𝑁)))
50	48, 49	sylib 208	. 2 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ Fin ∧ (1...𝑁) ⊆ 𝐴) → ∃𝑎 𝑎:((𝑁 + 1)...(#‘𝐴))–1-1-onto→(𝐴 ∖ (1...𝑁)))
51		simpl1 1064	. . . . 5 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ Fin ∧ (1...𝑁) ⊆ 𝐴) ∧ 𝑎:((𝑁 + 1)...(#‘𝐴))–1-1-onto→(𝐴 ∖ (1...𝑁))) → 𝑁 ∈ ℕ0)
52	51	nn0zd 11480	. . . 4 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ Fin ∧ (1...𝑁) ⊆ 𝐴) ∧ 𝑎:((𝑁 + 1)...(#‘𝐴))–1-1-onto→(𝐴 ∖ (1...𝑁))) → 𝑁 ∈ ℤ)
53		simpl2 1065	. . . . . 6 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ Fin ∧ (1...𝑁) ⊆ 𝐴) ∧ 𝑎:((𝑁 + 1)...(#‘𝐴))–1-1-onto→(𝐴 ∖ (1...𝑁))) → 𝐴 ∈ Fin)
54		hashcl 13147	. . . . . 6 ⊢ (𝐴 ∈ Fin → (#‘𝐴) ∈ ℕ0)
55	53, 54	syl 17	. . . . 5 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ Fin ∧ (1...𝑁) ⊆ 𝐴) ∧ 𝑎:((𝑁 + 1)...(#‘𝐴))–1-1-onto→(𝐴 ∖ (1...𝑁))) → (#‘𝐴) ∈ ℕ0)
56	55	nn0zd 11480	. . . 4 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ Fin ∧ (1...𝑁) ⊆ 𝐴) ∧ 𝑎:((𝑁 + 1)...(#‘𝐴))–1-1-onto→(𝐴 ∖ (1...𝑁))) → (#‘𝐴) ∈ ℤ)
57		nn0addge2 11340	. . . . . . 7 ⊢ ((𝑁 ∈ ℝ ∧ (#‘(𝐴 ∖ (1...𝑁))) ∈ ℕ0) → 𝑁 ≤ ((#‘(𝐴 ∖ (1...𝑁))) + 𝑁))
58	2, 30, 57	syl2anc 693	. . . . . 6 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ Fin ∧ (1...𝑁) ⊆ 𝐴) → 𝑁 ≤ ((#‘(𝐴 ∖ (1...𝑁))) + 𝑁))
59	58, 25	breqtrrd 4681	. . . . 5 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ Fin ∧ (1...𝑁) ⊆ 𝐴) → 𝑁 ≤ (#‘𝐴))
60	59	adantr 481	. . . 4 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ Fin ∧ (1...𝑁) ⊆ 𝐴) ∧ 𝑎:((𝑁 + 1)...(#‘𝐴))–1-1-onto→(𝐴 ∖ (1...𝑁))) → 𝑁 ≤ (#‘𝐴))
61		eluz2 11693	. . . 4 ⊢ ((#‘𝐴) ∈ (ℤ≥‘𝑁) ↔ (𝑁 ∈ ℤ ∧ (#‘𝐴) ∈ ℤ ∧ 𝑁 ≤ (#‘𝐴)))
62	52, 56, 60, 61	syl3anbrc 1246	. . 3 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ Fin ∧ (1...𝑁) ⊆ 𝐴) ∧ 𝑎:((𝑁 + 1)...(#‘𝐴))–1-1-onto→(𝐴 ∖ (1...𝑁))) → (#‘𝐴) ∈ (ℤ≥‘𝑁))
63		vex 3203	. . . . 5 ⊢ 𝑎 ∈ V
64		ovex 6678	. . . . . 6 ⊢ (1...𝑁) ∈ V
65		resiexg 7102	. . . . . 6 ⊢ ((1...𝑁) ∈ V → ( I ↾ (1...𝑁)) ∈ V)
66	64, 65	ax-mp 5	. . . . 5 ⊢ ( I ↾ (1...𝑁)) ∈ V
67	63, 66	unex 6956	. . . 4 ⊢ (𝑎 ∪ ( I ↾ (1...𝑁))) ∈ V
68	67	a1i 11	. . 3 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ Fin ∧ (1...𝑁) ⊆ 𝐴) ∧ 𝑎:((𝑁 + 1)...(#‘𝐴))–1-1-onto→(𝐴 ∖ (1...𝑁))) → (𝑎 ∪ ( I ↾ (1...𝑁))) ∈ V)
69		simpr 477	. . . . 5 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ Fin ∧ (1...𝑁) ⊆ 𝐴) ∧ 𝑎:((𝑁 + 1)...(#‘𝐴))–1-1-onto→(𝐴 ∖ (1...𝑁))) → 𝑎:((𝑁 + 1)...(#‘𝐴))–1-1-onto→(𝐴 ∖ (1...𝑁)))
70		f1oi 6174	. . . . . 6 ⊢ ( I ↾ (1...𝑁)):(1...𝑁)–1-1-onto→(1...𝑁)
71	70	a1i 11	. . . . 5 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ Fin ∧ (1...𝑁) ⊆ 𝐴) ∧ 𝑎:((𝑁 + 1)...(#‘𝐴))–1-1-onto→(𝐴 ∖ (1...𝑁))) → ( I ↾ (1...𝑁)):(1...𝑁)–1-1-onto→(1...𝑁))
72		incom 3805	. . . . . 6 ⊢ (((𝑁 + 1)...(#‘𝐴)) ∩ (1...𝑁)) = ((1...𝑁) ∩ ((𝑁 + 1)...(#‘𝐴)))
73	51	nn0red 11352	. . . . . . . 8 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ Fin ∧ (1...𝑁) ⊆ 𝐴) ∧ 𝑎:((𝑁 + 1)...(#‘𝐴))–1-1-onto→(𝐴 ∖ (1...𝑁))) → 𝑁 ∈ ℝ)
74	73	ltp1d 10954	. . . . . . 7 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ Fin ∧ (1...𝑁) ⊆ 𝐴) ∧ 𝑎:((𝑁 + 1)...(#‘𝐴))–1-1-onto→(𝐴 ∖ (1...𝑁))) → 𝑁 < (𝑁 + 1))
75		fzdisj 12368	. . . . . . 7 ⊢ (𝑁 < (𝑁 + 1) → ((1...𝑁) ∩ ((𝑁 + 1)...(#‘𝐴))) = ∅)
76	74, 75	syl 17	. . . . . 6 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ Fin ∧ (1...𝑁) ⊆ 𝐴) ∧ 𝑎:((𝑁 + 1)...(#‘𝐴))–1-1-onto→(𝐴 ∖ (1...𝑁))) → ((1...𝑁) ∩ ((𝑁 + 1)...(#‘𝐴))) = ∅)
77	72, 76	syl5eq 2668	. . . . 5 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ Fin ∧ (1...𝑁) ⊆ 𝐴) ∧ 𝑎:((𝑁 + 1)...(#‘𝐴))–1-1-onto→(𝐴 ∖ (1...𝑁))) → (((𝑁 + 1)...(#‘𝐴)) ∩ (1...𝑁)) = ∅)
78	12	a1i 11	. . . . 5 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ Fin ∧ (1...𝑁) ⊆ 𝐴) ∧ 𝑎:((𝑁 + 1)...(#‘𝐴))–1-1-onto→(𝐴 ∖ (1...𝑁))) → ((𝐴 ∖ (1...𝑁)) ∩ (1...𝑁)) = ∅)
79		f1oun 6156	. . . . 5 ⊢ (((𝑎:((𝑁 + 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...𝑁)))
80	69, 71, 77, 78, 79	syl22anc 1327	. . . 4 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ Fin ∧ (1...𝑁) ⊆ 𝐴) ∧ 𝑎:((𝑁 + 1)...(#‘𝐴))–1-1-onto→(𝐴 ∖ (1...𝑁))) → (𝑎 ∪ ( I ↾ (1...𝑁))):(((𝑁 + 1)...(#‘𝐴)) ∪ (1...𝑁))–1-1-onto→((𝐴 ∖ (1...𝑁)) ∪ (1...𝑁)))
81		fzsplit1nn0 37317	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ0 ∧ (#‘𝐴) ∈ ℕ0 ∧ 𝑁 ≤ (#‘𝐴)) → (1...(#‘𝐴)) = ((1...𝑁) ∪ ((𝑁 + 1)...(#‘𝐴))))
82	51, 55, 60, 81	syl3anc 1326	. . . . . 6 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ Fin ∧ (1...𝑁) ⊆ 𝐴) ∧ 𝑎:((𝑁 + 1)...(#‘𝐴))–1-1-onto→(𝐴 ∖ (1...𝑁))) → (1...(#‘𝐴)) = ((1...𝑁) ∪ ((𝑁 + 1)...(#‘𝐴))))
83		uncom 3757	. . . . . 6 ⊢ (((𝑁 + 1)...(#‘𝐴)) ∪ (1...𝑁)) = ((1...𝑁) ∪ ((𝑁 + 1)...(#‘𝐴)))
84	82, 83	syl6reqr 2675	. . . . 5 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ Fin ∧ (1...𝑁) ⊆ 𝐴) ∧ 𝑎:((𝑁 + 1)...(#‘𝐴))–1-1-onto→(𝐴 ∖ (1...𝑁))) → (((𝑁 + 1)...(#‘𝐴)) ∪ (1...𝑁)) = (1...(#‘𝐴)))
85		simpl3 1066	. . . . . . 7 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ Fin ∧ (1...𝑁) ⊆ 𝐴) ∧ 𝑎:((𝑁 + 1)...(#‘𝐴))–1-1-onto→(𝐴 ∖ (1...𝑁))) → (1...𝑁) ⊆ 𝐴)
86	85, 18	sylib 208	. . . . . 6 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ Fin ∧ (1...𝑁) ⊆ 𝐴) ∧ 𝑎:((𝑁 + 1)...(#‘𝐴))–1-1-onto→(𝐴 ∖ (1...𝑁))) → ((1...𝑁) ∪ (𝐴 ∖ (1...𝑁))) = 𝐴)
87	16, 86	syl5eq 2668	. . . . 5 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ Fin ∧ (1...𝑁) ⊆ 𝐴) ∧ 𝑎:((𝑁 + 1)...(#‘𝐴))–1-1-onto→(𝐴 ∖ (1...𝑁))) → ((𝐴 ∖ (1...𝑁)) ∪ (1...𝑁)) = 𝐴)
88		f1oeq23 6130	. . . . 5 ⊢ (((((𝑁 + 1)...(#‘𝐴)) ∪ (1...𝑁)) = (1...(#‘𝐴)) ∧ ((𝐴 ∖ (1...𝑁)) ∪ (1...𝑁)) = 𝐴) → ((𝑎 ∪ ( I ↾ (1...𝑁))):(((𝑁 + 1)...(#‘𝐴)) ∪ (1...𝑁))–1-1-onto→((𝐴 ∖ (1...𝑁)) ∪ (1...𝑁)) ↔ (𝑎 ∪ ( I ↾ (1...𝑁))):(1...(#‘𝐴))–1-1-onto→𝐴))
89	84, 87, 88	syl2anc 693	. . . 4 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ Fin ∧ (1...𝑁) ⊆ 𝐴) ∧ 𝑎:((𝑁 + 1)...(#‘𝐴))–1-1-onto→(𝐴 ∖ (1...𝑁))) → ((𝑎 ∪ ( I ↾ (1...𝑁))):(((𝑁 + 1)...(#‘𝐴)) ∪ (1...𝑁))–1-1-onto→((𝐴 ∖ (1...𝑁)) ∪ (1...𝑁)) ↔ (𝑎 ∪ ( I ↾ (1...𝑁))):(1...(#‘𝐴))–1-1-onto→𝐴))
90	80, 89	mpbid 222	. . 3 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ Fin ∧ (1...𝑁) ⊆ 𝐴) ∧ 𝑎:((𝑁 + 1)...(#‘𝐴))–1-1-onto→(𝐴 ∖ (1...𝑁))) → (𝑎 ∪ ( I ↾ (1...𝑁))):(1...(#‘𝐴))–1-1-onto→𝐴)
91		resundir 5411	. . . 4 ⊢ ((𝑎 ∪ ( I ↾ (1...𝑁))) ↾ (1...𝑁)) = ((𝑎 ↾ (1...𝑁)) ∪ (( I ↾ (1...𝑁)) ↾ (1...𝑁)))
92		dmres 5419	. . . . . . . 8 ⊢ dom (𝑎 ↾ (1...𝑁)) = ((1...𝑁) ∩ dom 𝑎)
93		f1odm 6141	. . . . . . . . . . 11 ⊢ (𝑎:((𝑁 + 1)...(#‘𝐴))–1-1-onto→(𝐴 ∖ (1...𝑁)) → dom 𝑎 = ((𝑁 + 1)...(#‘𝐴)))
94	93	adantl 482	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ Fin ∧ (1...𝑁) ⊆ 𝐴) ∧ 𝑎:((𝑁 + 1)...(#‘𝐴))–1-1-onto→(𝐴 ∖ (1...𝑁))) → dom 𝑎 = ((𝑁 + 1)...(#‘𝐴)))
95	94	ineq2d 3814	. . . . . . . . 9 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ Fin ∧ (1...𝑁) ⊆ 𝐴) ∧ 𝑎:((𝑁 + 1)...(#‘𝐴))–1-1-onto→(𝐴 ∖ (1...𝑁))) → ((1...𝑁) ∩ dom 𝑎) = ((1...𝑁) ∩ ((𝑁 + 1)...(#‘𝐴))))
96	95, 76	eqtrd 2656	. . . . . . . 8 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ Fin ∧ (1...𝑁) ⊆ 𝐴) ∧ 𝑎:((𝑁 + 1)...(#‘𝐴))–1-1-onto→(𝐴 ∖ (1...𝑁))) → ((1...𝑁) ∩ dom 𝑎) = ∅)
97	92, 96	syl5eq 2668	. . . . . . 7 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ Fin ∧ (1...𝑁) ⊆ 𝐴) ∧ 𝑎:((𝑁 + 1)...(#‘𝐴))–1-1-onto→(𝐴 ∖ (1...𝑁))) → dom (𝑎 ↾ (1...𝑁)) = ∅)
98		relres 5426	. . . . . . . 8 ⊢ Rel (𝑎 ↾ (1...𝑁))
99		reldm0 5343	. . . . . . . 8 ⊢ (Rel (𝑎 ↾ (1...𝑁)) → ((𝑎 ↾ (1...𝑁)) = ∅ ↔ dom (𝑎 ↾ (1...𝑁)) = ∅))
100	98, 99	ax-mp 5	. . . . . . 7 ⊢ ((𝑎 ↾ (1...𝑁)) = ∅ ↔ dom (𝑎 ↾ (1...𝑁)) = ∅)
101	97, 100	sylibr 224	. . . . . 6 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ Fin ∧ (1...𝑁) ⊆ 𝐴) ∧ 𝑎:((𝑁 + 1)...(#‘𝐴))–1-1-onto→(𝐴 ∖ (1...𝑁))) → (𝑎 ↾ (1...𝑁)) = ∅)
102		residm 5430	. . . . . . 7 ⊢ (( I ↾ (1...𝑁)) ↾ (1...𝑁)) = ( I ↾ (1...𝑁))
103	102	a1i 11	. . . . . 6 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ Fin ∧ (1...𝑁) ⊆ 𝐴) ∧ 𝑎:((𝑁 + 1)...(#‘𝐴))–1-1-onto→(𝐴 ∖ (1...𝑁))) → (( I ↾ (1...𝑁)) ↾ (1...𝑁)) = ( I ↾ (1...𝑁)))
104	101, 103	uneq12d 3768	. . . . 5 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ Fin ∧ (1...𝑁) ⊆ 𝐴) ∧ 𝑎:((𝑁 + 1)...(#‘𝐴))–1-1-onto→(𝐴 ∖ (1...𝑁))) → ((𝑎 ↾ (1...𝑁)) ∪ (( I ↾ (1...𝑁)) ↾ (1...𝑁))) = (∅ ∪ ( I ↾ (1...𝑁))))
105		uncom 3757	. . . . . 6 ⊢ (∅ ∪ ( I ↾ (1...𝑁))) = (( I ↾ (1...𝑁)) ∪ ∅)
106		un0 3967	. . . . . 6 ⊢ (( I ↾ (1...𝑁)) ∪ ∅) = ( I ↾ (1...𝑁))
107	105, 106	eqtri 2644	. . . . 5 ⊢ (∅ ∪ ( I ↾ (1...𝑁))) = ( I ↾ (1...𝑁))
108	104, 107	syl6eq 2672	. . . 4 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ Fin ∧ (1...𝑁) ⊆ 𝐴) ∧ 𝑎:((𝑁 + 1)...(#‘𝐴))–1-1-onto→(𝐴 ∖ (1...𝑁))) → ((𝑎 ↾ (1...𝑁)) ∪ (( I ↾ (1...𝑁)) ↾ (1...𝑁))) = ( I ↾ (1...𝑁)))
109	91, 108	syl5eq 2668	. . 3 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ Fin ∧ (1...𝑁) ⊆ 𝐴) ∧ 𝑎:((𝑁 + 1)...(#‘𝐴))–1-1-onto→(𝐴 ∖ (1...𝑁))) → ((𝑎 ∪ ( I ↾ (1...𝑁))) ↾ (1...𝑁)) = ( I ↾ (1...𝑁)))
110		oveq2 6658	. . . . . 6 ⊢ (𝑑 = (#‘𝐴) → (1...𝑑) = (1...(#‘𝐴)))
111		f1oeq2 6128	. . . . . 6 ⊢ ((1...𝑑) = (1...(#‘𝐴)) → (𝑒:(1...𝑑)–1-1-onto→𝐴 ↔ 𝑒:(1...(#‘𝐴))–1-1-onto→𝐴))
112	110, 111	syl 17	. . . . 5 ⊢ (𝑑 = (#‘𝐴) → (𝑒:(1...𝑑)–1-1-onto→𝐴 ↔ 𝑒:(1...(#‘𝐴))–1-1-onto→𝐴))
113	112	anbi1d 741	. . . 4 ⊢ (𝑑 = (#‘𝐴) → ((𝑒:(1...𝑑)–1-1-onto→𝐴 ∧ (𝑒 ↾ (1...𝑁)) = ( I ↾ (1...𝑁))) ↔ (𝑒:(1...(#‘𝐴))–1-1-onto→𝐴 ∧ (𝑒 ↾ (1...𝑁)) = ( I ↾ (1...𝑁)))))
114		f1oeq1 6127	. . . . 5 ⊢ (𝑒 = (𝑎 ∪ ( I ↾ (1...𝑁))) → (𝑒:(1...(#‘𝐴))–1-1-onto→𝐴 ↔ (𝑎 ∪ ( I ↾ (1...𝑁))):(1...(#‘𝐴))–1-1-onto→𝐴))
115		reseq1 5390	. . . . . 6 ⊢ (𝑒 = (𝑎 ∪ ( I ↾ (1...𝑁))) → (𝑒 ↾ (1...𝑁)) = ((𝑎 ∪ ( I ↾ (1...𝑁))) ↾ (1...𝑁)))
116	115	eqeq1d 2624	. . . . 5 ⊢ (𝑒 = (𝑎 ∪ ( I ↾ (1...𝑁))) → ((𝑒 ↾ (1...𝑁)) = ( I ↾ (1...𝑁)) ↔ ((𝑎 ∪ ( I ↾ (1...𝑁))) ↾ (1...𝑁)) = ( I ↾ (1...𝑁))))
117	114, 116	anbi12d 747	. . . 4 ⊢ (𝑒 = (𝑎 ∪ ( I ↾ (1...𝑁))) → ((𝑒:(1...(#‘𝐴))–1-1-onto→𝐴 ∧ (𝑒 ↾ (1...𝑁)) = ( I ↾ (1...𝑁))) ↔ ((𝑎 ∪ ( I ↾ (1...𝑁))):(1...(#‘𝐴))–1-1-onto→𝐴 ∧ ((𝑎 ∪ ( I ↾ (1...𝑁))) ↾ (1...𝑁)) = ( I ↾ (1...𝑁)))))
118	113, 117	rspc2ev 3324	. . 3 ⊢ (((#‘𝐴) ∈ (ℤ≥‘𝑁) ∧ (𝑎 ∪ ( I ↾ (1...𝑁))) ∈ V ∧ ((𝑎 ∪ ( I ↾ (1...𝑁))):(1...(#‘𝐴))–1-1-onto→𝐴 ∧ ((𝑎 ∪ ( I ↾ (1...𝑁))) ↾ (1...𝑁)) = ( I ↾ (1...𝑁)))) → ∃𝑑 ∈ (ℤ≥‘𝑁)∃𝑒 ∈ V (𝑒:(1...𝑑)–1-1-onto→𝐴 ∧ (𝑒 ↾ (1...𝑁)) = ( I ↾ (1...𝑁))))
119	62, 68, 90, 109, 118	syl112anc 1330	. 2 ⊢ (((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ Fin ∧ (1...𝑁) ⊆ 𝐴) ∧ 𝑎:((𝑁 + 1)...(#‘𝐴))–1-1-onto→(𝐴 ∖ (1...𝑁))) → ∃𝑑 ∈ (ℤ≥‘𝑁)∃𝑒 ∈ V (𝑒:(1...𝑑)–1-1-onto→𝐴 ∧ (𝑒 ↾ (1...𝑁)) = ( I ↾ (1...𝑁))))
120	50, 119	exlimddv 1863	1 ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ Fin ∧ (1...𝑁) ⊆ 𝐴) → ∃𝑑 ∈ (ℤ≥‘𝑁)∃𝑒 ∈ V (𝑒:(1...𝑑)–1-1-onto→𝐴 ∧ (𝑒 ↾ (1...𝑁)) = ( I ↾ (1...𝑁))))

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384   ∧ w3a 1037   = wceq 1483  ∃wex 1704   ∈ wcel 1990  ∃wrex 2913  Vcvv 3200   ∖ cdif 3571   ∪ cun 3572   ∩ cin 3573   ⊆ wss 3574  ∅c0 3915   class class class wbr 4653   I cid 5023  dom cdm 5114   ↾ cres 5116  Rel wrel 5119  –1-1-onto→wf1o 5887  ‘cfv 5888  (class class class)co 6650   ≈ cen 7952  Fincfn 7955  ℂcc 9934  ℝcr 9935  1c1 9937   + caddc 9939   < clt 10074   ≤ cle 10075  ℕ₀cn0 11292  ℤcz 11377  ℤ_≥cuz 11687  ...cfz 12326  #chash 13117

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-1st 7168  df-2nd 7169  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-oadd 7564  df-er 7742  df-en 7956  df-dom 7957  df-sdom 7958  df-fin 7959  df-card 8765  df-cda 8990  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-nn 11021  df-n0 11293  df-z 11378  df-uz 11688  df-fz 12327  df-hash 13118

This theorem is referenced by:  eldioph2  37325