eldioph2lem1

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

		Ref	Expression
	Assertion	eldioph2lem1	$⊢ (N \in ℕ_{0} \land A \in Fin \land (1 \dots N) \subseteq A) \to \exists d \in ℤ_{\geq N} \exists e \in V (e : (1 \dots d) \underset{1-1 onto}{⟶} A \land {e ↾}_{(1 \dots N)} = {I ↾}_{(1 \dots N)})$

Proof

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

Metamath Proof Explorer

Theorem eldioph2lem1

Proof