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		incom	$⊢ ((1 \dots A) ∖ (1 \dots N)) \cap (1 \dots N) = (1 \dots N) \cap ((1 \dots A) ∖ (1 \dots N))$
15		disjdif	$⊢ (1 \dots N) \cap ((1 \dots A) ∖ (1 \dots N)) = \emptyset$
16	14 15	eqtri	$⊢ ((1 \dots A) ∖ (1 \dots N)) \cap (1 \dots N) = \emptyset$
17	16	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$
18		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)$
19	18	frnd	$⊢ a : (1 \dots A) ∖ (1 \dots N) \underset{1-1}{⟶} S ∖ (1 \dots N) \to ran a \subseteq S ∖ (1 \dots N)$
20	19	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)$
21	20	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)$
22		incom	$⊢ (S ∖ (1 \dots N)) \cap (1 \dots N) = (1 \dots N) \cap (S ∖ (1 \dots N))$
23		disjdif	$⊢ (1 \dots N) \cap (S ∖ (1 \dots N)) = \emptyset$
24	22 23	eqtri	$⊢ (S ∖ (1 \dots N)) \cap (1 \dots N) = \emptyset$
25	21 24	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$
26		ss0	$⊢ ran a \cap (1 \dots N) \subseteq \emptyset \to ran a \cap (1 \dots N) = \emptyset$
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 ran a \cap (1 \dots N) = \emptyset$
28		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)$
29	11 13 17 27 28	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)$
30		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)$
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 (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)$
32		uncom	$⊢ ((1 \dots A) ∖ (1 \dots N)) \cup (1 \dots N) = (1 \dots N) \cup ((1 \dots A) ∖ (1 \dots N))$
33		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}$
34		fzss2	$⊢ A \in ℤ_{\geq N} \to (1 \dots N) \subseteq (1 \dots A)$
35	33 34	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)$
36		undif	$⊢ (1 \dots N) \subseteq (1 \dots A) \leftrightarrow (1 \dots N) \cup ((1 \dots A) ∖ (1 \dots N)) = (1 \dots A)$
37	35 36	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)$
38	32 37	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)$
39		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))$
40	38 39	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))$
41	31 40	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)$
42	19	difss2d	$⊢ a : (1 \dots A) ∖ (1 \dots N) \underset{1-1}{⟶} S ∖ (1 \dots N) \to ran a \subseteq S$
43	42	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$
44		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$
45	43 44	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$
46		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$
47	41 45 46	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$
48		resundir	$⊢ {(a \cup ({I ↾}_{(1 \dots N)})) ↾}_{(1 \dots N)} = ({a ↾}_{(1 \dots N)}) \cup ({({I ↾}_{(1 \dots N)}) ↾}_{(1 \dots N)})$
49		dmres	$⊢ dom ({a ↾}_{(1 \dots N)}) = (1 \dots N) \cap dom a$
50		incom	$⊢ (1 \dots N) \cap dom a = dom a \cap (1 \dots N)$
51		f1dm	$⊢ a : (1 \dots A) ∖ (1 \dots N) \underset{1-1}{⟶} S ∖ (1 \dots N) \to dom a = (1 \dots A) ∖ (1 \dots N)$
52	51	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)$
53	52	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)$
54	53 16	syl6eq	$⊢ (((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$
55	50 54	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$
56	49 55	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$
57		relres	$⊢ Rel ({a ↾}_{(1 \dots N)})$
58		reldm0	$⊢ Rel ({a ↾}_{(1 \dots N)}) \to ({a ↾}_{(1 \dots N)} = \emptyset \leftrightarrow dom ({a ↾}_{(1 \dots N)}) = \emptyset)$
59	57 58	ax-mp	$⊢ {a ↾}_{(1 \dots N)} = \emptyset \leftrightarrow dom ({a ↾}_{(1 \dots N)}) = \emptyset$
60	56 59	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$
61		residm	$⊢ {({I ↾}_{(1 \dots N)}) ↾}_{(1 \dots N)} = {I ↾}_{(1 \dots N)}$
62	61	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)}$
63	60 62	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)})$
64		uncom	$⊢ \emptyset \cup ({I ↾}_{(1 \dots N)}) = ({I ↾}_{(1 \dots N)}) \cup \emptyset$
65		un0	$⊢ ({I ↾}_{(1 \dots N)}) \cup \emptyset = {I ↾}_{(1 \dots N)}$
66	64 65	eqtri	$⊢ \emptyset \cup ({I ↾}_{(1 \dots N)}) = {I ↾}_{(1 \dots N)}$
67	63 66	syl6eq	$⊢ (((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)}$
68	48 67	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)}$
69		vex	$⊢ a \in V$
70		ovex	$⊢ (1 \dots N) \in V$
71		resiexg	$⊢ (1 \dots N) \in V \to {I ↾}_{(1 \dots N)} \in V$
72	70 71	ax-mp	$⊢ {I ↾}_{(1 \dots N)} \in V$
73	69 72	unex	$⊢ a \cup ({I ↾}_{(1 \dots N)}) \in V$
74		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)$
75		reseq1	$⊢ c = a \cup ({I ↾}_{(1 \dots N)}) \to {c ↾}_{(1 \dots N)} = {(a \cup ({I ↾}_{(1 \dots N)})) ↾}_{(1 \dots N)}$
76	75	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)})$
77	74 76	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)}))$
78	73 77	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)})$
79	47 68 78	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)})$
80	9 79	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