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		incom	$⊢ (A ∖ (1 \dots N)) \cap (1 \dots N) = (1 \dots N) \cap (A ∖ (1 \dots N))$
11		disjdif	$⊢ (1 \dots N) \cap (A ∖ (1 \dots N)) = \emptyset$
12	10 11	eqtri	$⊢ (A ∖ (1 \dots N)) \cap (1 \dots N) = \emptyset$
13	12	a1i	$⊢ (N \in ℕ_{0} \land A \in Fin \land (1 \dots N) \subseteq A) \to (A ∖ (1 \dots N)) \cap (1 \dots N) = \emptyset$
14		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)\|$
15	8 9 13 14	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)\|$
16		uncom	$⊢ (A ∖ (1 \dots N)) \cup (1 \dots N) = (1 \dots N) \cup (A ∖ (1 \dots N))$
17		simp3	$⊢ (N \in ℕ_{0} \land A \in Fin \land (1 \dots N) \subseteq A) \to (1 \dots N) \subseteq A$
18		undif	$⊢ (1 \dots N) \subseteq A \leftrightarrow (1 \dots N) \cup (A ∖ (1 \dots N)) = A$
19	17 18	sylib	$⊢ (N \in ℕ_{0} \land A \in Fin \land (1 \dots N) \subseteq A) \to (1 \dots N) \cup (A ∖ (1 \dots N)) = A$
20	16 19	syl5eq	$⊢ (N \in ℕ_{0} \land A \in Fin \land (1 \dots N) \subseteq A) \to (A ∖ (1 \dots N)) \cup (1 \dots N) = A$
21	20	fveq2d	$⊢ (N \in ℕ_{0} \land A \in Fin \land (1 \dots N) \subseteq A) \to \|(A ∖ (1 \dots N)) \cup (1 \dots N)\| = \|A\|$
22		hashfz1	$⊢ N \in ℕ_{0} \to \|(1 \dots N)\| = N$
23	22	3ad2ant1	$⊢ (N \in ℕ_{0} \land A \in Fin \land (1 \dots N) \subseteq A) \to \|(1 \dots N)\| = N$
24	23	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$
25	15 21 24	3eqtr3d	$⊢ (N \in ℕ_{0} \land A \in Fin \land (1 \dots N) \subseteq A) \to \|A\| = \|A ∖ (1 \dots N)\| + N$
26	6 25	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)$
27	26	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)\|$
28		1zzd	$⊢ (N \in ℕ_{0} \land A \in Fin \land (1 \dots N) \subseteq A) \to 1 \in ℤ$
29		hashcl	$⊢ A ∖ (1 \dots N) \in Fin \to \|A ∖ (1 \dots N)\| \in ℕ_{0}$
30	8 29	syl	$⊢ (N \in ℕ_{0} \land A \in Fin \land (1 \dots N) \subseteq A) \to \|A ∖ (1 \dots N)\| \in ℕ_{0}$
31	30	nn0zd	$⊢ (N \in ℕ_{0} \land A \in Fin \land (1 \dots N) \subseteq A) \to \|A ∖ (1 \dots N)\| \in ℤ$
32		nn0z	$⊢ N \in ℕ_{0} \to N \in ℤ$
33	32	3ad2ant1	$⊢ (N \in ℕ_{0} \land A \in Fin \land (1 \dots N) \subseteq A) \to N \in ℤ$
34		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)$
35	28 31 33 34	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)$
36	35	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)\|)$
37		fzfi	$⊢ (1 + N \dots \|A ∖ (1 \dots N)\| + N) \in Fin$
38		fzfi	$⊢ (1 \dots \|A ∖ (1 \dots N)\|) \in Fin$
39		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)\|))$
40	37 38 39	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)\|)$
41	36 40	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)\|)\|$
42		hashfz1	$⊢ \|A ∖ (1 \dots N)\| \in ℕ_{0} \to \|(1 \dots \|A ∖ (1 \dots N)\|)\| = \|A ∖ (1 \dots N)\|$
43	30 42	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)\|$
44	27 41 43	3eqtrd	$⊢ (N \in ℕ_{0} \land A \in Fin \land (1 \dots N) \subseteq A) \to \|(N + 1 \dots \|A\|)\| = \|A ∖ (1 \dots N)\|$
45		fzfi	$⊢ (N + 1 \dots \|A\|) \in Fin$
46		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)))$
47	45 8 46	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)))$
48	44 47	mpbid	$⊢ (N \in ℕ_{0} \land A \in Fin \land (1 \dots N) \subseteq A) \to (N + 1 \dots \|A\|) \approx (A ∖ (1 \dots N))$
49		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)$
50	48 49	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)$
51		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}$
52	51	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 ℤ$
53		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$
54		hashcl	$⊢ A \in Fin \to \|A\| \in ℕ_{0}$
55	53 54	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}$
56	55	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 ℤ$
57		nn0addge2	$⊢ (N \in ℝ \land \|A ∖ (1 \dots N)\| \in ℕ_{0}) \to N \leq \|A ∖ (1 \dots N)\| + N$
58	2 30 57	syl2anc	$⊢ (N \in ℕ_{0} \land A \in Fin \land (1 \dots N) \subseteq A) \to N \leq \|A ∖ (1 \dots N)\| + N$
59	58 25	breqtrrd	$⊢ (N \in ℕ_{0} \land A \in Fin \land (1 \dots N) \subseteq A) \to N \leq \|A\|$
60	59	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\|$
61		eluz2	$⊢ \|A\| \in ℤ_{\geq N} \leftrightarrow (N \in ℤ \land \|A\| \in ℤ \land N \leq \|A\|)$
62	52 56 60 61	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}$
63		vex	$⊢ a \in V$
64		ovex	$⊢ (1 \dots N) \in V$
65		resiexg	$⊢ (1 \dots N) \in V \to {I ↾}_{(1 \dots N)} \in V$
66	64 65	ax-mp	$⊢ {I ↾}_{(1 \dots N)} \in V$
67	63 66	unex	$⊢ a \cup ({I ↾}_{(1 \dots N)}) \in V$
68	67	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$
69		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)$
70		f1oi	$⊢ ({I ↾}_{(1 \dots N)}) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)$
71	70	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)$
72		incom	$⊢ (N + 1 \dots \|A\|) \cap (1 \dots N) = (1 \dots N) \cap (N + 1 \dots \|A\|)$
73	51	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 ℝ$
74	73	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$
75		fzdisj	$⊢ N < N + 1 \to (1 \dots N) \cap (N + 1 \dots \|A\|) = \emptyset$
76	74 75	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$
77	72 76	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$
78	12	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$
79		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)$
80	69 71 77 78 79	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)$
81		uncom	$⊢ (N + 1 \dots \|A\|) \cup (1 \dots N) = (1 \dots N) \cup (N + 1 \dots \|A\|)$
82		fzsplit1nn0	$⊢ (N \in ℕ_{0} \land \|A\| \in ℕ_{0} \land N \leq \|A\|) \to (1 \dots \|A\|) = (1 \dots N) \cup (N + 1 \dots \|A\|)$
83	51 55 60 82	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\|)$
84	81 83	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\|)$
85		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$
86	85 18	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$
87	16 86	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$
88		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)$
89	84 87 88	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)$
90	80 89	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$
91		resundir	$⊢ {(a \cup ({I ↾}_{(1 \dots N)})) ↾}_{(1 \dots N)} = ({a ↾}_{(1 \dots N)}) \cup ({({I ↾}_{(1 \dots N)}) ↾}_{(1 \dots N)})$
92		dmres	$⊢ dom ({a ↾}_{(1 \dots N)}) = (1 \dots N) \cap dom a$
93		f1odm	$⊢ a : (N + 1 \dots \|A\|) \underset{1-1 onto}{⟶} A ∖ (1 \dots N) \to dom a = (N + 1 \dots \|A\|)$
94	93	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\|)$
95	94	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\|)$
96	95 76	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$
97	92 96	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$
98		relres	$⊢ Rel ({a ↾}_{(1 \dots N)})$
99		reldm0	$⊢ Rel ({a ↾}_{(1 \dots N)}) \to ({a ↾}_{(1 \dots N)} = \emptyset \leftrightarrow dom ({a ↾}_{(1 \dots N)}) = \emptyset)$
100	98 99	ax-mp	$⊢ {a ↾}_{(1 \dots N)} = \emptyset \leftrightarrow dom ({a ↾}_{(1 \dots N)}) = \emptyset$
101	97 100	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$
102		residm	$⊢ {({I ↾}_{(1 \dots N)}) ↾}_{(1 \dots N)} = {I ↾}_{(1 \dots N)}$
103	102	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)}$
104	101 103	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)})$
105		uncom	$⊢ \emptyset \cup ({I ↾}_{(1 \dots N)}) = ({I ↾}_{(1 \dots N)}) \cup \emptyset$
106		un0	$⊢ ({I ↾}_{(1 \dots N)}) \cup \emptyset = {I ↾}_{(1 \dots N)}$
107	105 106	eqtri	$⊢ \emptyset \cup ({I ↾}_{(1 \dots N)}) = {I ↾}_{(1 \dots N)}$
108	104 107	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)}$
109	91 108	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)}$
110		oveq2	$⊢ d = \|A\| \to (1 \dots d) = (1 \dots \|A\|)$
111	110	f1oeq2d	$⊢ d = \|A\| \to (e : (1 \dots d) \underset{1-1 onto}{⟶} A \leftrightarrow e : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)$
112	111	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)}))$
113		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)$
114		reseq1	$⊢ e = a \cup ({I ↾}_{(1 \dots N)}) \to {e ↾}_{(1 \dots N)} = {(a \cup ({I ↾}_{(1 \dots N)})) ↾}_{(1 \dots N)}$
115	114	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)})$
116	113 115	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)}))$
117	112 116	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)})$
118	62 68 90 109 117	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)})$
119	50 118	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