eldioph2lem2

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

		Ref	Expression
	Assertion	eldioph2lem2	$⊢ ((N \in ℕ_{0} \land \neg S \in Fin) \land ((1 \dots N) \subseteq S \land A \in ℤ_{\geq N})) \to \exists c (c : (1 \dots A) \underset{1-1}{⟶} S \land {c ↾}_{(1 \dots N)} = {I ↾}_{(1 \dots N)})$

Proof

Step	Hyp	Ref	Expression
1		simplr	$⊢ ((N \in ℕ_{0} \land \neg S \in Fin) \land ((1 \dots N) \subseteq S \land A \in ℤ_{\geq N})) \to \neg S \in Fin$
2		fzfi	$⊢ (1 \dots N) \in Fin$
3		difinf	$⊢ (\neg S \in Fin \land (1 \dots N) \in Fin) \to \neg S ∖ (1 \dots N) \in Fin$
4	1 2 3	sylancl	$⊢ ((N \in ℕ_{0} \land \neg S \in Fin) \land ((1 \dots N) \subseteq S \land A \in ℤ_{\geq N})) \to \neg S ∖ (1 \dots N) \in Fin$
5		fzfi	$⊢ (1 \dots A) \in Fin$
6		diffi	$⊢ (1 \dots A) \in Fin \to (1 \dots A) ∖ (1 \dots N) \in Fin$
7	5 6	ax-mp	$⊢ (1 \dots A) ∖ (1 \dots N) \in Fin$
8		isinffi	$⊢ (\neg S ∖ (1 \dots N) \in Fin \land (1 \dots A) ∖ (1 \dots N) \in Fin) \to \exists a a : (1 \dots A) ∖ (1 \dots N) \underset{1-1}{⟶} S ∖ (1 \dots N)$
9	4 7 8	sylancl	$⊢ ((N \in ℕ_{0} \land \neg S \in Fin) \land ((1 \dots N) \subseteq S \land A \in ℤ_{\geq N})) \to \exists a a : (1 \dots A) ∖ (1 \dots N) \underset{1-1}{⟶} S ∖ (1 \dots N)$
10		f1f1orn	$⊢ a : (1 \dots A) ∖ (1 \dots N) \underset{1-1}{⟶} S ∖ (1 \dots N) \to a : (1 \dots A) ∖ (1 \dots N) \underset{1-1 onto}{⟶} ran a$
11	10	adantl	$⊢ (((N \in ℕ_{0} \land \neg S \in Fin) \land ((1 \dots N) \subseteq S \land A \in ℤ_{\geq N})) \land a : (1 \dots A) ∖ (1 \dots N) \underset{1-1}{⟶} S ∖ (1 \dots N)) \to a : (1 \dots A) ∖ (1 \dots N) \underset{1-1 onto}{⟶} ran a$
12		f1oi	$⊢ ({I ↾}_{(1 \dots N)}) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)$
13	12	a1i	$⊢ (((N \in ℕ_{0} \land \neg S \in Fin) \land ((1 \dots N) \subseteq S \land A \in ℤ_{\geq N})) \land a : (1 \dots A) ∖ (1 \dots N) \underset{1-1}{⟶} S ∖ (1 \dots N)) \to ({I ↾}_{(1 \dots N)}) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)$
14		disjdifr	$⊢ ((1 \dots A) ∖ (1 \dots N)) \cap (1 \dots N) = \emptyset$
15	14	a1i	$⊢ (((N \in ℕ_{0} \land \neg S \in Fin) \land ((1 \dots N) \subseteq S \land A \in ℤ_{\geq N})) \land a : (1 \dots A) ∖ (1 \dots N) \underset{1-1}{⟶} S ∖ (1 \dots N)) \to ((1 \dots A) ∖ (1 \dots N)) \cap (1 \dots N) = \emptyset$
16		f1f	$⊢ a : (1 \dots A) ∖ (1 \dots N) \underset{1-1}{⟶} S ∖ (1 \dots N) \to a : (1 \dots A) ∖ (1 \dots N) ⟶ S ∖ (1 \dots N)$
17	16	frnd	$⊢ a : (1 \dots A) ∖ (1 \dots N) \underset{1-1}{⟶} S ∖ (1 \dots N) \to ran a \subseteq S ∖ (1 \dots N)$
18	17	adantl	$⊢ (((N \in ℕ_{0} \land \neg S \in Fin) \land ((1 \dots N) \subseteq S \land A \in ℤ_{\geq N})) \land a : (1 \dots A) ∖ (1 \dots N) \underset{1-1}{⟶} S ∖ (1 \dots N)) \to ran a \subseteq S ∖ (1 \dots N)$
19	18	ssrind	$⊢ (((N \in ℕ_{0} \land \neg S \in Fin) \land ((1 \dots N) \subseteq S \land A \in ℤ_{\geq N})) \land a : (1 \dots A) ∖ (1 \dots N) \underset{1-1}{⟶} S ∖ (1 \dots N)) \to ran a \cap (1 \dots N) \subseteq (S ∖ (1 \dots N)) \cap (1 \dots N)$
20		disjdifr	$⊢ (S ∖ (1 \dots N)) \cap (1 \dots N) = \emptyset$
21	19 20	sseqtrdi	$⊢ (((N \in ℕ_{0} \land \neg S \in Fin) \land ((1 \dots N) \subseteq S \land A \in ℤ_{\geq N})) \land a : (1 \dots A) ∖ (1 \dots N) \underset{1-1}{⟶} S ∖ (1 \dots N)) \to ran a \cap (1 \dots N) \subseteq \emptyset$
22		ss0	$⊢ ran a \cap (1 \dots N) \subseteq \emptyset \to ran a \cap (1 \dots N) = \emptyset$
23	21 22	syl	$⊢ (((N \in ℕ_{0} \land \neg S \in Fin) \land ((1 \dots N) \subseteq S \land A \in ℤ_{\geq N})) \land a : (1 \dots A) ∖ (1 \dots N) \underset{1-1}{⟶} S ∖ (1 \dots N)) \to ran a \cap (1 \dots N) = \emptyset$
24		f1oun	$⊢ ((a : (1 \dots A) ∖ (1 \dots N) \underset{1-1 onto}{⟶} ran a \land ({I ↾}_{(1 \dots N)}) : (1 \dots N) \underset{1-1 onto}{⟶} (1 \dots N)) \land (((1 \dots A) ∖ (1 \dots N)) \cap (1 \dots N) = \emptyset \land ran a \cap (1 \dots N) = \emptyset)) \to (a \cup ({I ↾}_{(1 \dots N)})) : ((1 \dots A) ∖ (1 \dots N)) \cup (1 \dots N) \underset{1-1 onto}{⟶} ran a \cup (1 \dots N)$
25	11 13 15 23 24	syl22anc	$⊢ (((N \in ℕ_{0} \land \neg S \in Fin) \land ((1 \dots N) \subseteq S \land A \in ℤ_{\geq N})) \land a : (1 \dots A) ∖ (1 \dots N) \underset{1-1}{⟶} S ∖ (1 \dots N)) \to (a \cup ({I ↾}_{(1 \dots N)})) : ((1 \dots A) ∖ (1 \dots N)) \cup (1 \dots N) \underset{1-1 onto}{⟶} ran a \cup (1 \dots N)$
26		f1of1	$⊢ (a \cup ({I ↾}_{(1 \dots N)})) : ((1 \dots A) ∖ (1 \dots N)) \cup (1 \dots N) \underset{1-1 onto}{⟶} ran a \cup (1 \dots N) \to (a \cup ({I ↾}_{(1 \dots N)})) : ((1 \dots A) ∖ (1 \dots N)) \cup (1 \dots N) \underset{1-1}{⟶} ran a \cup (1 \dots N)$
27	25 26	syl	$⊢ (((N \in ℕ_{0} \land \neg S \in Fin) \land ((1 \dots N) \subseteq S \land A \in ℤ_{\geq N})) \land a : (1 \dots A) ∖ (1 \dots N) \underset{1-1}{⟶} S ∖ (1 \dots N)) \to (a \cup ({I ↾}_{(1 \dots N)})) : ((1 \dots A) ∖ (1 \dots N)) \cup (1 \dots N) \underset{1-1}{⟶} ran a \cup (1 \dots N)$
28		uncom	$⊢ ((1 \dots A) ∖ (1 \dots N)) \cup (1 \dots N) = (1 \dots N) \cup ((1 \dots A) ∖ (1 \dots N))$
29		simplrr	$⊢ (((N \in ℕ_{0} \land \neg S \in Fin) \land ((1 \dots N) \subseteq S \land A \in ℤ_{\geq N})) \land a : (1 \dots A) ∖ (1 \dots N) \underset{1-1}{⟶} S ∖ (1 \dots N)) \to A \in ℤ_{\geq N}$
30		fzss2	$⊢ A \in ℤ_{\geq N} \to (1 \dots N) \subseteq (1 \dots A)$
31	29 30	syl	$⊢ (((N \in ℕ_{0} \land \neg S \in Fin) \land ((1 \dots N) \subseteq S \land A \in ℤ_{\geq N})) \land a : (1 \dots A) ∖ (1 \dots N) \underset{1-1}{⟶} S ∖ (1 \dots N)) \to (1 \dots N) \subseteq (1 \dots A)$
32		undif	$⊢ (1 \dots N) \subseteq (1 \dots A) \leftrightarrow (1 \dots N) \cup ((1 \dots A) ∖ (1 \dots N)) = (1 \dots A)$
33	31 32	sylib	$⊢ (((N \in ℕ_{0} \land \neg S \in Fin) \land ((1 \dots N) \subseteq S \land A \in ℤ_{\geq N})) \land a : (1 \dots A) ∖ (1 \dots N) \underset{1-1}{⟶} S ∖ (1 \dots N)) \to (1 \dots N) \cup ((1 \dots A) ∖ (1 \dots N)) = (1 \dots A)$
34	28 33	syl5eq	$⊢ (((N \in ℕ_{0} \land \neg S \in Fin) \land ((1 \dots N) \subseteq S \land A \in ℤ_{\geq N})) \land a : (1 \dots A) ∖ (1 \dots N) \underset{1-1}{⟶} S ∖ (1 \dots N)) \to ((1 \dots A) ∖ (1 \dots N)) \cup (1 \dots N) = (1 \dots A)$
35		f1eq2	$⊢ ((1 \dots A) ∖ (1 \dots N)) \cup (1 \dots N) = (1 \dots A) \to ((a \cup ({I ↾}_{(1 \dots N)})) : ((1 \dots A) ∖ (1 \dots N)) \cup (1 \dots N) \underset{1-1}{⟶} ran a \cup (1 \dots N) \leftrightarrow (a \cup ({I ↾}_{(1 \dots N)})) : (1 \dots A) \underset{1-1}{⟶} ran a \cup (1 \dots N))$
36	34 35	syl	$⊢ (((N \in ℕ_{0} \land \neg S \in Fin) \land ((1 \dots N) \subseteq S \land A \in ℤ_{\geq N})) \land a : (1 \dots A) ∖ (1 \dots N) \underset{1-1}{⟶} S ∖ (1 \dots N)) \to ((a \cup ({I ↾}_{(1 \dots N)})) : ((1 \dots A) ∖ (1 \dots N)) \cup (1 \dots N) \underset{1-1}{⟶} ran a \cup (1 \dots N) \leftrightarrow (a \cup ({I ↾}_{(1 \dots N)})) : (1 \dots A) \underset{1-1}{⟶} ran a \cup (1 \dots N))$
37	27 36	mpbid	$⊢ (((N \in ℕ_{0} \land \neg S \in Fin) \land ((1 \dots N) \subseteq S \land A \in ℤ_{\geq N})) \land a : (1 \dots A) ∖ (1 \dots N) \underset{1-1}{⟶} S ∖ (1 \dots N)) \to (a \cup ({I ↾}_{(1 \dots N)})) : (1 \dots A) \underset{1-1}{⟶} ran a \cup (1 \dots N)$
38	17	difss2d	$⊢ a : (1 \dots A) ∖ (1 \dots N) \underset{1-1}{⟶} S ∖ (1 \dots N) \to ran a \subseteq S$
39	38	adantl	$⊢ (((N \in ℕ_{0} \land \neg S \in Fin) \land ((1 \dots N) \subseteq S \land A \in ℤ_{\geq N})) \land a : (1 \dots A) ∖ (1 \dots N) \underset{1-1}{⟶} S ∖ (1 \dots N)) \to ran a \subseteq S$
40		simplrl	$⊢ (((N \in ℕ_{0} \land \neg S \in Fin) \land ((1 \dots N) \subseteq S \land A \in ℤ_{\geq N})) \land a : (1 \dots A) ∖ (1 \dots N) \underset{1-1}{⟶} S ∖ (1 \dots N)) \to (1 \dots N) \subseteq S$
41	39 40	unssd	$⊢ (((N \in ℕ_{0} \land \neg S \in Fin) \land ((1 \dots N) \subseteq S \land A \in ℤ_{\geq N})) \land a : (1 \dots A) ∖ (1 \dots N) \underset{1-1}{⟶} S ∖ (1 \dots N)) \to ran a \cup (1 \dots N) \subseteq S$
42		f1ss	$⊢ ((a \cup ({I ↾}_{(1 \dots N)})) : (1 \dots A) \underset{1-1}{⟶} ran a \cup (1 \dots N) \land ran a \cup (1 \dots N) \subseteq S) \to (a \cup ({I ↾}_{(1 \dots N)})) : (1 \dots A) \underset{1-1}{⟶} S$
43	37 41 42	syl2anc	$⊢ (((N \in ℕ_{0} \land \neg S \in Fin) \land ((1 \dots N) \subseteq S \land A \in ℤ_{\geq N})) \land a : (1 \dots A) ∖ (1 \dots N) \underset{1-1}{⟶} S ∖ (1 \dots N)) \to (a \cup ({I ↾}_{(1 \dots N)})) : (1 \dots A) \underset{1-1}{⟶} S$
44		resundir	$⊢ {(a \cup ({I ↾}_{(1 \dots N)})) ↾}_{(1 \dots N)} = ({a ↾}_{(1 \dots N)}) \cup ({({I ↾}_{(1 \dots N)}) ↾}_{(1 \dots N)})$
45		dmres	$⊢ dom ({a ↾}_{(1 \dots N)}) = (1 \dots N) \cap dom a$
46		incom	$⊢ (1 \dots N) \cap dom a = dom a \cap (1 \dots N)$
47		f1dm	$⊢ a : (1 \dots A) ∖ (1 \dots N) \underset{1-1}{⟶} S ∖ (1 \dots N) \to dom a = (1 \dots A) ∖ (1 \dots N)$
48	47	adantl	$⊢ (((N \in ℕ_{0} \land \neg S \in Fin) \land ((1 \dots N) \subseteq S \land A \in ℤ_{\geq N})) \land a : (1 \dots A) ∖ (1 \dots N) \underset{1-1}{⟶} S ∖ (1 \dots N)) \to dom a = (1 \dots A) ∖ (1 \dots N)$
49	48	ineq1d	$⊢ (((N \in ℕ_{0} \land \neg S \in Fin) \land ((1 \dots N) \subseteq S \land A \in ℤ_{\geq N})) \land a : (1 \dots A) ∖ (1 \dots N) \underset{1-1}{⟶} S ∖ (1 \dots N)) \to dom a \cap (1 \dots N) = ((1 \dots A) ∖ (1 \dots N)) \cap (1 \dots N)$
50	49 14	eqtrdi	$⊢ (((N \in ℕ_{0} \land \neg S \in Fin) \land ((1 \dots N) \subseteq S \land A \in ℤ_{\geq N})) \land a : (1 \dots A) ∖ (1 \dots N) \underset{1-1}{⟶} S ∖ (1 \dots N)) \to dom a \cap (1 \dots N) = \emptyset$
51	46 50	syl5eq	$⊢ (((N \in ℕ_{0} \land \neg S \in Fin) \land ((1 \dots N) \subseteq S \land A \in ℤ_{\geq N})) \land a : (1 \dots A) ∖ (1 \dots N) \underset{1-1}{⟶} S ∖ (1 \dots N)) \to (1 \dots N) \cap dom a = \emptyset$
52	45 51	syl5eq	$⊢ (((N \in ℕ_{0} \land \neg S \in Fin) \land ((1 \dots N) \subseteq S \land A \in ℤ_{\geq N})) \land a : (1 \dots A) ∖ (1 \dots N) \underset{1-1}{⟶} S ∖ (1 \dots N)) \to dom ({a ↾}_{(1 \dots N)}) = \emptyset$
53		relres	$⊢ Rel ({a ↾}_{(1 \dots N)})$
54		reldm0	$⊢ Rel ({a ↾}_{(1 \dots N)}) \to ({a ↾}_{(1 \dots N)} = \emptyset \leftrightarrow dom ({a ↾}_{(1 \dots N)}) = \emptyset)$
55	53 54	ax-mp	$⊢ {a ↾}_{(1 \dots N)} = \emptyset \leftrightarrow dom ({a ↾}_{(1 \dots N)}) = \emptyset$
56	52 55	sylibr	$⊢ (((N \in ℕ_{0} \land \neg S \in Fin) \land ((1 \dots N) \subseteq S \land A \in ℤ_{\geq N})) \land a : (1 \dots A) ∖ (1 \dots N) \underset{1-1}{⟶} S ∖ (1 \dots N)) \to {a ↾}_{(1 \dots N)} = \emptyset$
57		residm	$⊢ {({I ↾}_{(1 \dots N)}) ↾}_{(1 \dots N)} = {I ↾}_{(1 \dots N)}$
58	57	a1i	$⊢ (((N \in ℕ_{0} \land \neg S \in Fin) \land ((1 \dots N) \subseteq S \land A \in ℤ_{\geq N})) \land a : (1 \dots A) ∖ (1 \dots N) \underset{1-1}{⟶} S ∖ (1 \dots N)) \to {({I ↾}_{(1 \dots N)}) ↾}_{(1 \dots N)} = {I ↾}_{(1 \dots N)}$
59	56 58	uneq12d	$⊢ (((N \in ℕ_{0} \land \neg S \in Fin) \land ((1 \dots N) \subseteq S \land A \in ℤ_{\geq N})) \land a : (1 \dots A) ∖ (1 \dots N) \underset{1-1}{⟶} S ∖ (1 \dots N)) \to ({a ↾}_{(1 \dots N)}) \cup ({({I ↾}_{(1 \dots N)}) ↾}_{(1 \dots N)}) = \emptyset \cup ({I ↾}_{(1 \dots N)})$
60		uncom	$⊢ \emptyset \cup ({I ↾}_{(1 \dots N)}) = ({I ↾}_{(1 \dots N)}) \cup \emptyset$
61		un0	$⊢ ({I ↾}_{(1 \dots N)}) \cup \emptyset = {I ↾}_{(1 \dots N)}$
62	60 61	eqtri	$⊢ \emptyset \cup ({I ↾}_{(1 \dots N)}) = {I ↾}_{(1 \dots N)}$
63	59 62	eqtrdi	$⊢ (((N \in ℕ_{0} \land \neg S \in Fin) \land ((1 \dots N) \subseteq S \land A \in ℤ_{\geq N})) \land a : (1 \dots A) ∖ (1 \dots N) \underset{1-1}{⟶} S ∖ (1 \dots N)) \to ({a ↾}_{(1 \dots N)}) \cup ({({I ↾}_{(1 \dots N)}) ↾}_{(1 \dots N)}) = {I ↾}_{(1 \dots N)}$
64	44 63	syl5eq	$⊢ (((N \in ℕ_{0} \land \neg S \in Fin) \land ((1 \dots N) \subseteq S \land A \in ℤ_{\geq N})) \land a : (1 \dots A) ∖ (1 \dots N) \underset{1-1}{⟶} S ∖ (1 \dots N)) \to {(a \cup ({I ↾}_{(1 \dots N)})) ↾}_{(1 \dots N)} = {I ↾}_{(1 \dots N)}$
65		vex	$⊢ a \in V$
66		ovex	$⊢ (1 \dots N) \in V$
67		resiexg	$⊢ (1 \dots N) \in V \to {I ↾}_{(1 \dots N)} \in V$
68	66 67	ax-mp	$⊢ {I ↾}_{(1 \dots N)} \in V$
69	65 68	unex	$⊢ a \cup ({I ↾}_{(1 \dots N)}) \in V$
70		f1eq1	$⊢ c = a \cup ({I ↾}_{(1 \dots N)}) \to (c : (1 \dots A) \underset{1-1}{⟶} S \leftrightarrow (a \cup ({I ↾}_{(1 \dots N)})) : (1 \dots A) \underset{1-1}{⟶} S)$
71		reseq1	$⊢ c = a \cup ({I ↾}_{(1 \dots N)}) \to {c ↾}_{(1 \dots N)} = {(a \cup ({I ↾}_{(1 \dots N)})) ↾}_{(1 \dots N)}$
72	71	eqeq1d	$⊢ c = a \cup ({I ↾}_{(1 \dots N)}) \to ({c ↾}_{(1 \dots N)} = {I ↾}_{(1 \dots N)} \leftrightarrow {(a \cup ({I ↾}_{(1 \dots N)})) ↾}_{(1 \dots N)} = {I ↾}_{(1 \dots N)})$
73	70 72	anbi12d	$⊢ c = a \cup ({I ↾}_{(1 \dots N)}) \to ((c : (1 \dots A) \underset{1-1}{⟶} S \land {c ↾}_{(1 \dots N)} = {I ↾}_{(1 \dots N)}) \leftrightarrow ((a \cup ({I ↾}_{(1 \dots N)})) : (1 \dots A) \underset{1-1}{⟶} S \land {(a \cup ({I ↾}_{(1 \dots N)})) ↾}_{(1 \dots N)} = {I ↾}_{(1 \dots N)}))$
74	69 73	spcev	$⊢ ((a \cup ({I ↾}_{(1 \dots N)})) : (1 \dots A) \underset{1-1}{⟶} S \land {(a \cup ({I ↾}_{(1 \dots N)})) ↾}_{(1 \dots N)} = {I ↾}_{(1 \dots N)}) \to \exists c (c : (1 \dots A) \underset{1-1}{⟶} S \land {c ↾}_{(1 \dots N)} = {I ↾}_{(1 \dots N)})$
75	43 64 74	syl2anc	$⊢ (((N \in ℕ_{0} \land \neg S \in Fin) \land ((1 \dots N) \subseteq S \land A \in ℤ_{\geq N})) \land a : (1 \dots A) ∖ (1 \dots N) \underset{1-1}{⟶} S ∖ (1 \dots N)) \to \exists c (c : (1 \dots A) \underset{1-1}{⟶} S \land {c ↾}_{(1 \dots N)} = {I ↾}_{(1 \dots N)})$
76	9 75	exlimddv	$⊢ ((N \in ℕ_{0} \land \neg S \in Fin) \land ((1 \dots N) \subseteq S \land A \in ℤ_{\geq N})) \to \exists c (c : (1 \dots A) \underset{1-1}{⟶} S \land {c ↾}_{(1 \dots N)} = {I ↾}_{(1 \dots N)})$

Metamath Proof Explorer

Theorem eldioph2lem2

Proof