fin23lem28

Description: Lemma for fin23 . The residual is also one-to-one. This preserves the induction invariant. (Contributed by Stefan O'Rear, 2-Nov-2014)

	Ref	Expression
Hypotheses	fin23lem.a	$⊢ U = {seq}_{ω} ((i \in ω, u \in V ⟼ if (t (i) \cap u = \emptyset, u, t (i) \cap u)), ⋃ ran t)$
	fin23lem17.f	$⊢ F = \{g \| \forall a \in ({𝒫 g}^{ω}) (\forall x \in ω a (suc x) \subseteq a (x) \to ⋂ ran a \in ran a)\}$
	fin23lem.b	$⊢ P = \{v \in ω \| ⋂ ran U \subseteq t (v)\}$
	fin23lem.c	$⊢ Q = (w \in ω ⟼ (ι x \in P \| (x \cap P) \approx w))$
	fin23lem.d	$⊢ R = (w \in ω ⟼ (ι x \in (ω ∖ P) \| (x \cap (ω ∖ P)) \approx w))$
	fin23lem.e	$⊢ Z = if (P \in Fin, t \circ R, (z \in P ⟼ t (z) ∖ ⋂ ran U) \circ Q)$
Assertion	fin23lem28	$⊢ t : ω \underset{1-1}{⟶} V \to Z : ω \underset{1-1}{⟶} V$

Proof

Step	Hyp	Ref	Expression
1		fin23lem.a	$⊢ U = {seq}_{ω} ((i \in ω, u \in V ⟼ if (t (i) \cap u = \emptyset, u, t (i) \cap u)), ⋃ ran t)$
2		fin23lem17.f	$⊢ F = \{g \| \forall a \in ({𝒫 g}^{ω}) (\forall x \in ω a (suc x) \subseteq a (x) \to ⋂ ran a \in ran a)\}$
3		fin23lem.b	$⊢ P = \{v \in ω \| ⋂ ran U \subseteq t (v)\}$
4		fin23lem.c	$⊢ Q = (w \in ω ⟼ (ι x \in P \| (x \cap P) \approx w))$
5		fin23lem.d	$⊢ R = (w \in ω ⟼ (ι x \in (ω ∖ P) \| (x \cap (ω ∖ P)) \approx w))$
6		fin23lem.e	$⊢ Z = if (P \in Fin, t \circ R, (z \in P ⟼ t (z) ∖ ⋂ ran U) \circ Q)$
7		eqif	$⊢ Z = if (P \in Fin, t \circ R, (z \in P ⟼ t (z) ∖ ⋂ ran U) \circ Q) \leftrightarrow ((P \in Fin \land Z = t \circ R) \lor (\neg P \in Fin \land Z = (z \in P ⟼ t (z) ∖ ⋂ ran U) \circ Q))$
8	6 7	mpbi	$⊢ ((P \in Fin \land Z = t \circ R) \lor (\neg P \in Fin \land Z = (z \in P ⟼ t (z) ∖ ⋂ ran U) \circ Q))$
9		difss	$⊢ ω ∖ P \subseteq ω$
10		ominf	$⊢ \neg ω \in Fin$
11	3	ssrab3	$⊢ P \subseteq ω$
12		undif	$⊢ P \subseteq ω \leftrightarrow P \cup (ω ∖ P) = ω$
13	11 12	mpbi	$⊢ P \cup (ω ∖ P) = ω$
14		unfi	$⊢ (P \in Fin \land ω ∖ P \in Fin) \to P \cup (ω ∖ P) \in Fin$
15	13 14	eqeltrrid	$⊢ (P \in Fin \land ω ∖ P \in Fin) \to ω \in Fin$
16	15	ex	$⊢ P \in Fin \to (ω ∖ P \in Fin \to ω \in Fin)$
17	10 16	mtoi	$⊢ P \in Fin \to \neg ω ∖ P \in Fin$
18	5	fin23lem22	$⊢ (ω ∖ P \subseteq ω \land \neg ω ∖ P \in Fin) \to R : ω \underset{1-1 onto}{⟶} ω ∖ P$
19	9 17 18	sylancr	$⊢ P \in Fin \to R : ω \underset{1-1 onto}{⟶} ω ∖ P$
20	19	adantl	$⊢ (t : ω \underset{1-1}{⟶} V \land P \in Fin) \to R : ω \underset{1-1 onto}{⟶} ω ∖ P$
21		f1of1	$⊢ R : ω \underset{1-1 onto}{⟶} ω ∖ P \to R : ω \underset{1-1}{⟶} ω ∖ P$
22		f1ss	$⊢ (R : ω \underset{1-1}{⟶} ω ∖ P \land ω ∖ P \subseteq ω) \to R : ω \underset{1-1}{⟶} ω$
23	9 22	mpan2	$⊢ R : ω \underset{1-1}{⟶} ω ∖ P \to R : ω \underset{1-1}{⟶} ω$
24	20 21 23	3syl	$⊢ (t : ω \underset{1-1}{⟶} V \land P \in Fin) \to R : ω \underset{1-1}{⟶} ω$
25		f1co	$⊢ (t : ω \underset{1-1}{⟶} V \land R : ω \underset{1-1}{⟶} ω) \to (t \circ R) : ω \underset{1-1}{⟶} V$
26	24 25	syldan	$⊢ (t : ω \underset{1-1}{⟶} V \land P \in Fin) \to (t \circ R) : ω \underset{1-1}{⟶} V$
27		f1eq1	$⊢ Z = t \circ R \to (Z : ω \underset{1-1}{⟶} V \leftrightarrow (t \circ R) : ω \underset{1-1}{⟶} V)$
28	26 27	syl5ibrcom	$⊢ (t : ω \underset{1-1}{⟶} V \land P \in Fin) \to (Z = t \circ R \to Z : ω \underset{1-1}{⟶} V)$
29	28	impr	$⊢ (t : ω \underset{1-1}{⟶} V \land (P \in Fin \land Z = t \circ R)) \to Z : ω \underset{1-1}{⟶} V$
30		fvex	$⊢ t (z) \in V$
31	30	difexi	$⊢ t (z) ∖ ⋂ ran U \in V$
32	31	rgenw	$⊢ \forall z \in P t (z) ∖ ⋂ ran U \in V$
33		eqid	$⊢ (z \in P ⟼ t (z) ∖ ⋂ ran U) = (z \in P ⟼ t (z) ∖ ⋂ ran U)$
34	33	fmpt	$⊢ \forall z \in P t (z) ∖ ⋂ ran U \in V \leftrightarrow (z \in P ⟼ t (z) ∖ ⋂ ran U) : P ⟶ V$
35	32 34	mpbi	$⊢ (z \in P ⟼ t (z) ∖ ⋂ ran U) : P ⟶ V$
36	35	a1i	$⊢ t : ω \underset{1-1}{⟶} V \to (z \in P ⟼ t (z) ∖ ⋂ ran U) : P ⟶ V$
37		fveq2	$⊢ z = a \to t (z) = t (a)$
38	37	difeq1d	$⊢ z = a \to t (z) ∖ ⋂ ran U = t (a) ∖ ⋂ ran U$
39		fvex	$⊢ t (a) \in V$
40	39	difexi	$⊢ t (a) ∖ ⋂ ran U \in V$
41	38 33 40	fvmpt	$⊢ a \in P \to (z \in P ⟼ t (z) ∖ ⋂ ran U) (a) = t (a) ∖ ⋂ ran U$
42	41	ad2antrl	$⊢ (t : ω \underset{1-1}{⟶} V \land (a \in P \land b \in P)) \to (z \in P ⟼ t (z) ∖ ⋂ ran U) (a) = t (a) ∖ ⋂ ran U$
43		fveq2	$⊢ z = b \to t (z) = t (b)$
44	43	difeq1d	$⊢ z = b \to t (z) ∖ ⋂ ran U = t (b) ∖ ⋂ ran U$
45		fvex	$⊢ t (b) \in V$
46	45	difexi	$⊢ t (b) ∖ ⋂ ran U \in V$
47	44 33 46	fvmpt	$⊢ b \in P \to (z \in P ⟼ t (z) ∖ ⋂ ran U) (b) = t (b) ∖ ⋂ ran U$
48	47	ad2antll	$⊢ (t : ω \underset{1-1}{⟶} V \land (a \in P \land b \in P)) \to (z \in P ⟼ t (z) ∖ ⋂ ran U) (b) = t (b) ∖ ⋂ ran U$
49	42 48	eqeq12d	$⊢ (t : ω \underset{1-1}{⟶} V \land (a \in P \land b \in P)) \to ((z \in P ⟼ t (z) ∖ ⋂ ran U) (a) = (z \in P ⟼ t (z) ∖ ⋂ ran U) (b) \leftrightarrow t (a) ∖ ⋂ ran U = t (b) ∖ ⋂ ran U)$
50		uneq2	$⊢ t (a) ∖ ⋂ ran U = t (b) ∖ ⋂ ran U \to ⋂ ran U \cup (t (a) ∖ ⋂ ran U) = ⋂ ran U \cup (t (b) ∖ ⋂ ran U)$
51		fveq2	$⊢ v = a \to t (v) = t (a)$
52	51	sseq2d	$⊢ v = a \to (⋂ ran U \subseteq t (v) \leftrightarrow ⋂ ran U \subseteq t (a))$
53	52 3	elrab2	$⊢ a \in P \leftrightarrow (a \in ω \land ⋂ ran U \subseteq t (a))$
54	53	simprbi	$⊢ a \in P \to ⋂ ran U \subseteq t (a)$
55	54	ad2antrl	$⊢ (t : ω \underset{1-1}{⟶} V \land (a \in P \land b \in P)) \to ⋂ ran U \subseteq t (a)$
56		undif	$⊢ ⋂ ran U \subseteq t (a) \leftrightarrow ⋂ ran U \cup (t (a) ∖ ⋂ ran U) = t (a)$
57	55 56	sylib	$⊢ (t : ω \underset{1-1}{⟶} V \land (a \in P \land b \in P)) \to ⋂ ran U \cup (t (a) ∖ ⋂ ran U) = t (a)$
58		fveq2	$⊢ v = b \to t (v) = t (b)$
59	58	sseq2d	$⊢ v = b \to (⋂ ran U \subseteq t (v) \leftrightarrow ⋂ ran U \subseteq t (b))$
60	59 3	elrab2	$⊢ b \in P \leftrightarrow (b \in ω \land ⋂ ran U \subseteq t (b))$
61	60	simprbi	$⊢ b \in P \to ⋂ ran U \subseteq t (b)$
62	61	ad2antll	$⊢ (t : ω \underset{1-1}{⟶} V \land (a \in P \land b \in P)) \to ⋂ ran U \subseteq t (b)$
63		undif	$⊢ ⋂ ran U \subseteq t (b) \leftrightarrow ⋂ ran U \cup (t (b) ∖ ⋂ ran U) = t (b)$
64	62 63	sylib	$⊢ (t : ω \underset{1-1}{⟶} V \land (a \in P \land b \in P)) \to ⋂ ran U \cup (t (b) ∖ ⋂ ran U) = t (b)$
65	57 64	eqeq12d	$⊢ (t : ω \underset{1-1}{⟶} V \land (a \in P \land b \in P)) \to (⋂ ran U \cup (t (a) ∖ ⋂ ran U) = ⋂ ran U \cup (t (b) ∖ ⋂ ran U) \leftrightarrow t (a) = t (b))$
66	50 65	imbitrid	$⊢ (t : ω \underset{1-1}{⟶} V \land (a \in P \land b \in P)) \to (t (a) ∖ ⋂ ran U = t (b) ∖ ⋂ ran U \to t (a) = t (b))$
67	11	sseli	$⊢ a \in P \to a \in ω$
68	11	sseli	$⊢ b \in P \to b \in ω$
69	67 68	anim12i	$⊢ (a \in P \land b \in P) \to (a \in ω \land b \in ω)$
70		f1fveq	$⊢ (t : ω \underset{1-1}{⟶} V \land (a \in ω \land b \in ω)) \to (t (a) = t (b) \leftrightarrow a = b)$
71	69 70	sylan2	$⊢ (t : ω \underset{1-1}{⟶} V \land (a \in P \land b \in P)) \to (t (a) = t (b) \leftrightarrow a = b)$
72	66 71	sylibd	$⊢ (t : ω \underset{1-1}{⟶} V \land (a \in P \land b \in P)) \to (t (a) ∖ ⋂ ran U = t (b) ∖ ⋂ ran U \to a = b)$
73	49 72	sylbid	$⊢ (t : ω \underset{1-1}{⟶} V \land (a \in P \land b \in P)) \to ((z \in P ⟼ t (z) ∖ ⋂ ran U) (a) = (z \in P ⟼ t (z) ∖ ⋂ ran U) (b) \to a = b)$
74	73	ralrimivva	$⊢ t : ω \underset{1-1}{⟶} V \to \forall a \in P \forall b \in P ((z \in P ⟼ t (z) ∖ ⋂ ran U) (a) = (z \in P ⟼ t (z) ∖ ⋂ ran U) (b) \to a = b)$
75		dff13	$⊢ (z \in P ⟼ t (z) ∖ ⋂ ran U) : P \underset{1-1}{⟶} V \leftrightarrow ((z \in P ⟼ t (z) ∖ ⋂ ran U) : P ⟶ V \land \forall a \in P \forall b \in P ((z \in P ⟼ t (z) ∖ ⋂ ran U) (a) = (z \in P ⟼ t (z) ∖ ⋂ ran U) (b) \to a = b))$
76	36 74 75	sylanbrc	$⊢ t : ω \underset{1-1}{⟶} V \to (z \in P ⟼ t (z) ∖ ⋂ ran U) : P \underset{1-1}{⟶} V$
77	4	fin23lem22	$⊢ (P \subseteq ω \land \neg P \in Fin) \to Q : ω \underset{1-1 onto}{⟶} P$
78		f1of1	$⊢ Q : ω \underset{1-1 onto}{⟶} P \to Q : ω \underset{1-1}{⟶} P$
79	77 78	syl	$⊢ (P \subseteq ω \land \neg P \in Fin) \to Q : ω \underset{1-1}{⟶} P$
80	11 79	mpan	$⊢ \neg P \in Fin \to Q : ω \underset{1-1}{⟶} P$
81		f1co	$⊢ ((z \in P ⟼ t (z) ∖ ⋂ ran U) : P \underset{1-1}{⟶} V \land Q : ω \underset{1-1}{⟶} P) \to ((z \in P ⟼ t (z) ∖ ⋂ ran U) \circ Q) : ω \underset{1-1}{⟶} V$
82	76 80 81	syl2an	$⊢ (t : ω \underset{1-1}{⟶} V \land \neg P \in Fin) \to ((z \in P ⟼ t (z) ∖ ⋂ ran U) \circ Q) : ω \underset{1-1}{⟶} V$
83		f1eq1	$⊢ Z = (z \in P ⟼ t (z) ∖ ⋂ ran U) \circ Q \to (Z : ω \underset{1-1}{⟶} V \leftrightarrow ((z \in P ⟼ t (z) ∖ ⋂ ran U) \circ Q) : ω \underset{1-1}{⟶} V)$
84	82 83	syl5ibrcom	$⊢ (t : ω \underset{1-1}{⟶} V \land \neg P \in Fin) \to (Z = (z \in P ⟼ t (z) ∖ ⋂ ran U) \circ Q \to Z : ω \underset{1-1}{⟶} V)$
85	84	impr	$⊢ (t : ω \underset{1-1}{⟶} V \land (\neg P \in Fin \land Z = (z \in P ⟼ t (z) ∖ ⋂ ran U) \circ Q)) \to Z : ω \underset{1-1}{⟶} V$
86	29 85	jaodan	$⊢ (t : ω \underset{1-1}{⟶} V \land ((P \in Fin \land Z = t \circ R) \lor (\neg P \in Fin \land Z = (z \in P ⟼ t (z) ∖ ⋂ ran U) \circ Q))) \to Z : ω \underset{1-1}{⟶} V$
87	8 86	mpan2	$⊢ t : ω \underset{1-1}{⟶} V \to Z : ω \underset{1-1}{⟶} V$

Metamath Proof Explorer

Theorem fin23lem28

Proof