fin23lem30

Description: Lemma for fin23 . The residual is disjoint from the common set. (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	fin23lem30	$⊢ Fun t \to ⋃ ran Z \cap ⋂ ran U = \emptyset$

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	7	biimpi	$⊢ Z = if (P \in Fin, t \circ R, (z \in P ⟼ t (z) ∖ ⋂ ran U) \circ Q) \to ((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		simpr	$⊢ (P \in Fin \land Fun t) \to Fun t$
10	5	funmpt2	$⊢ Fun R$
11		funco	$⊢ (Fun t \land Fun R) \to Fun (t \circ R)$
12	9 10 11	sylancl	$⊢ (P \in Fin \land Fun t) \to Fun (t \circ R)$
13		elunirn	$⊢ Fun (t \circ R) \to (a \in ⋃ ran (t \circ R) \leftrightarrow \exists b \in dom (t \circ R) a \in (t \circ R) (b))$
14	12 13	syl	$⊢ (P \in Fin \land Fun t) \to (a \in ⋃ ran (t \circ R) \leftrightarrow \exists b \in dom (t \circ R) a \in (t \circ R) (b))$
15		dmcoss	$⊢ dom (t \circ R) \subseteq dom R$
16	15	sseli	$⊢ b \in dom (t \circ R) \to b \in dom R$
17		fvco	$⊢ (Fun R \land b \in dom R) \to (t \circ R) (b) = t (R (b))$
18	10 17	mpan	$⊢ b \in dom R \to (t \circ R) (b) = t (R (b))$
19	18	adantl	$⊢ ((P \in Fin \land Fun t) \land b \in dom R) \to (t \circ R) (b) = t (R (b))$
20	19	eleq2d	$⊢ ((P \in Fin \land Fun t) \land b \in dom R) \to (a \in (t \circ R) (b) \leftrightarrow a \in t (R (b)))$
21		incom	$⊢ t (R (b)) \cap ⋂ ran U = ⋂ ran U \cap t (R (b))$
22		difss	$⊢ ω ∖ P \subseteq ω$
23		ominf	$⊢ \neg ω \in Fin$
24	3	ssrab3	$⊢ P \subseteq ω$
25		undif	$⊢ P \subseteq ω \leftrightarrow P \cup (ω ∖ P) = ω$
26	24 25	mpbi	$⊢ P \cup (ω ∖ P) = ω$
27		unfi	$⊢ (P \in Fin \land ω ∖ P \in Fin) \to P \cup (ω ∖ P) \in Fin$
28	26 27	eqeltrrid	$⊢ (P \in Fin \land ω ∖ P \in Fin) \to ω \in Fin$
29	28	ex	$⊢ P \in Fin \to (ω ∖ P \in Fin \to ω \in Fin)$
30	23 29	mtoi	$⊢ P \in Fin \to \neg ω ∖ P \in Fin$
31	30	ad2antrr	$⊢ ((P \in Fin \land Fun t) \land b \in dom R) \to \neg ω ∖ P \in Fin$
32	5	fin23lem22	$⊢ (ω ∖ P \subseteq ω \land \neg ω ∖ P \in Fin) \to R : ω \underset{1-1 onto}{⟶} ω ∖ P$
33	22 31 32	sylancr	$⊢ ((P \in Fin \land Fun t) \land b \in dom R) \to R : ω \underset{1-1 onto}{⟶} ω ∖ P$
34		f1of	$⊢ R : ω \underset{1-1 onto}{⟶} ω ∖ P \to R : ω ⟶ ω ∖ P$
35	33 34	syl	$⊢ ((P \in Fin \land Fun t) \land b \in dom R) \to R : ω ⟶ ω ∖ P$
36		simpr	$⊢ ((P \in Fin \land Fun t) \land b \in dom R) \to b \in dom R$
37	35	fdmd	$⊢ ((P \in Fin \land Fun t) \land b \in dom R) \to dom R = ω$
38	36 37	eleqtrd	$⊢ ((P \in Fin \land Fun t) \land b \in dom R) \to b \in ω$
39	35 38	ffvelcdmd	$⊢ ((P \in Fin \land Fun t) \land b \in dom R) \to R (b) \in (ω ∖ P)$
40	39	eldifbd	$⊢ ((P \in Fin \land Fun t) \land b \in dom R) \to \neg R (b) \in P$
41	3	eleq2i	$⊢ R (b) \in P \leftrightarrow R (b) \in \{v \in ω \| ⋂ ran U \subseteq t (v)\}$
42	40 41	sylnib	$⊢ ((P \in Fin \land Fun t) \land b \in dom R) \to \neg R (b) \in \{v \in ω \| ⋂ ran U \subseteq t (v)\}$
43	39	eldifad	$⊢ ((P \in Fin \land Fun t) \land b \in dom R) \to R (b) \in ω$
44		fveq2	$⊢ v = R (b) \to t (v) = t (R (b))$
45	44	sseq2d	$⊢ v = R (b) \to (⋂ ran U \subseteq t (v) \leftrightarrow ⋂ ran U \subseteq t (R (b)))$
46	45	elrab3	$⊢ R (b) \in ω \to (R (b) \in \{v \in ω \| ⋂ ran U \subseteq t (v)\} \leftrightarrow ⋂ ran U \subseteq t (R (b)))$
47	43 46	syl	$⊢ ((P \in Fin \land Fun t) \land b \in dom R) \to (R (b) \in \{v \in ω \| ⋂ ran U \subseteq t (v)\} \leftrightarrow ⋂ ran U \subseteq t (R (b)))$
48	42 47	mtbid	$⊢ ((P \in Fin \land Fun t) \land b \in dom R) \to \neg ⋂ ran U \subseteq t (R (b))$
49	1	fin23lem20	$⊢ R (b) \in ω \to (⋂ ran U \subseteq t (R (b)) \lor ⋂ ran U \cap t (R (b)) = \emptyset)$
50	43 49	syl	$⊢ ((P \in Fin \land Fun t) \land b \in dom R) \to (⋂ ran U \subseteq t (R (b)) \lor ⋂ ran U \cap t (R (b)) = \emptyset)$
51		orel1	$⊢ \neg ⋂ ran U \subseteq t (R (b)) \to ((⋂ ran U \subseteq t (R (b)) \lor ⋂ ran U \cap t (R (b)) = \emptyset) \to ⋂ ran U \cap t (R (b)) = \emptyset)$
52	48 50 51	sylc	$⊢ ((P \in Fin \land Fun t) \land b \in dom R) \to ⋂ ran U \cap t (R (b)) = \emptyset$
53	21 52	eqtrid	$⊢ ((P \in Fin \land Fun t) \land b \in dom R) \to t (R (b)) \cap ⋂ ran U = \emptyset$
54		disj	$⊢ t (R (b)) \cap ⋂ ran U = \emptyset \leftrightarrow \forall a \in t (R (b)) \neg a \in ⋂ ran U$
55	53 54	sylib	$⊢ ((P \in Fin \land Fun t) \land b \in dom R) \to \forall a \in t (R (b)) \neg a \in ⋂ ran U$
56		rsp	$⊢ \forall a \in t (R (b)) \neg a \in ⋂ ran U \to (a \in t (R (b)) \to \neg a \in ⋂ ran U)$
57	55 56	syl	$⊢ ((P \in Fin \land Fun t) \land b \in dom R) \to (a \in t (R (b)) \to \neg a \in ⋂ ran U)$
58	20 57	sylbid	$⊢ ((P \in Fin \land Fun t) \land b \in dom R) \to (a \in (t \circ R) (b) \to \neg a \in ⋂ ran U)$
59	58	ex	$⊢ (P \in Fin \land Fun t) \to (b \in dom R \to (a \in (t \circ R) (b) \to \neg a \in ⋂ ran U))$
60	16 59	syl5	$⊢ (P \in Fin \land Fun t) \to (b \in dom (t \circ R) \to (a \in (t \circ R) (b) \to \neg a \in ⋂ ran U))$
61	60	rexlimdv	$⊢ (P \in Fin \land Fun t) \to (\exists b \in dom (t \circ R) a \in (t \circ R) (b) \to \neg a \in ⋂ ran U)$
62	14 61	sylbid	$⊢ (P \in Fin \land Fun t) \to (a \in ⋃ ran (t \circ R) \to \neg a \in ⋂ ran U)$
63	62	ralrimiv	$⊢ (P \in Fin \land Fun t) \to \forall a \in ⋃ ran (t \circ R) \neg a \in ⋂ ran U$
64		disj	$⊢ ⋃ ran (t \circ R) \cap ⋂ ran U = \emptyset \leftrightarrow \forall a \in ⋃ ran (t \circ R) \neg a \in ⋂ ran U$
65	63 64	sylibr	$⊢ (P \in Fin \land Fun t) \to ⋃ ran (t \circ R) \cap ⋂ ran U = \emptyset$
66		rneq	$⊢ Z = t \circ R \to ran Z = ran (t \circ R)$
67	66	unieqd	$⊢ Z = t \circ R \to ⋃ ran Z = ⋃ ran (t \circ R)$
68	67	ineq1d	$⊢ Z = t \circ R \to ⋃ ran Z \cap ⋂ ran U = ⋃ ran (t \circ R) \cap ⋂ ran U$
69	68	eqeq1d	$⊢ Z = t \circ R \to (⋃ ran Z \cap ⋂ ran U = \emptyset \leftrightarrow ⋃ ran (t \circ R) \cap ⋂ ran U = \emptyset)$
70	65 69	imbitrrid	$⊢ Z = t \circ R \to ((P \in Fin \land Fun t) \to ⋃ ran Z \cap ⋂ ran U = \emptyset)$
71	70	expd	$⊢ Z = t \circ R \to (P \in Fin \to (Fun t \to ⋃ ran Z \cap ⋂ ran U = \emptyset))$
72	71	impcom	$⊢ (P \in Fin \land Z = t \circ R) \to (Fun t \to ⋃ ran Z \cap ⋂ ran U = \emptyset)$
73		rneq	$⊢ Z = (z \in P ⟼ t (z) ∖ ⋂ ran U) \circ Q \to ran Z = ran ((z \in P ⟼ t (z) ∖ ⋂ ran U) \circ Q)$
74	73	unieqd	$⊢ Z = (z \in P ⟼ t (z) ∖ ⋂ ran U) \circ Q \to ⋃ ran Z = ⋃ ran ((z \in P ⟼ t (z) ∖ ⋂ ran U) \circ Q)$
75	74	ineq1d	$⊢ Z = (z \in P ⟼ t (z) ∖ ⋂ ran U) \circ Q \to ⋃ ran Z \cap ⋂ ran U = ⋃ ran ((z \in P ⟼ t (z) ∖ ⋂ ran U) \circ Q) \cap ⋂ ran U$
76		rncoss	$⊢ ran ((z \in P ⟼ t (z) ∖ ⋂ ran U) \circ Q) \subseteq ran (z \in P ⟼ t (z) ∖ ⋂ ran U)$
77	76	unissi	$⊢ ⋃ ran ((z \in P ⟼ t (z) ∖ ⋂ ran U) \circ Q) \subseteq ⋃ ran (z \in P ⟼ t (z) ∖ ⋂ ran U)$
78		disj	$⊢ ⋃ ran (z \in P ⟼ t (z) ∖ ⋂ ran U) \cap ⋂ ran U = \emptyset \leftrightarrow \forall a \in ⋃ ran (z \in P ⟼ t (z) ∖ ⋂ ran U) \neg a \in ⋂ ran U$
79		eluniab	$⊢ a \in ⋃ \{b \| \exists z \in P b = t (z) ∖ ⋂ ran U\} \leftrightarrow \exists b (a \in b \land \exists z \in P b = t (z) ∖ ⋂ ran U)$
80		eleq2	$⊢ b = t (z) ∖ ⋂ ran U \to (a \in b \leftrightarrow a \in (t (z) ∖ ⋂ ran U))$
81		eldifn	$⊢ a \in (t (z) ∖ ⋂ ran U) \to \neg a \in ⋂ ran U$
82	80 81	biimtrdi	$⊢ b = t (z) ∖ ⋂ ran U \to (a \in b \to \neg a \in ⋂ ran U)$
83	82	rexlimivw	$⊢ \exists z \in P b = t (z) ∖ ⋂ ran U \to (a \in b \to \neg a \in ⋂ ran U)$
84	83	impcom	$⊢ (a \in b \land \exists z \in P b = t (z) ∖ ⋂ ran U) \to \neg a \in ⋂ ran U$
85	84	exlimiv	$⊢ \exists b (a \in b \land \exists z \in P b = t (z) ∖ ⋂ ran U) \to \neg a \in ⋂ ran U$
86	79 85	sylbi	$⊢ a \in ⋃ \{b \| \exists z \in P b = t (z) ∖ ⋂ ran U\} \to \neg a \in ⋂ ran U$
87		eqid	$⊢ (z \in P ⟼ t (z) ∖ ⋂ ran U) = (z \in P ⟼ t (z) ∖ ⋂ ran U)$
88	87	rnmpt	$⊢ ran (z \in P ⟼ t (z) ∖ ⋂ ran U) = \{b \| \exists z \in P b = t (z) ∖ ⋂ ran U\}$
89	88	unieqi	$⊢ ⋃ ran (z \in P ⟼ t (z) ∖ ⋂ ran U) = ⋃ \{b \| \exists z \in P b = t (z) ∖ ⋂ ran U\}$
90	86 89	eleq2s	$⊢ a \in ⋃ ran (z \in P ⟼ t (z) ∖ ⋂ ran U) \to \neg a \in ⋂ ran U$
91	78 90	mprgbir	$⊢ ⋃ ran (z \in P ⟼ t (z) ∖ ⋂ ran U) \cap ⋂ ran U = \emptyset$
92		ssdisj	$⊢ (⋃ ran ((z \in P ⟼ t (z) ∖ ⋂ ran U) \circ Q) \subseteq ⋃ ran (z \in P ⟼ t (z) ∖ ⋂ ran U) \land ⋃ ran (z \in P ⟼ t (z) ∖ ⋂ ran U) \cap ⋂ ran U = \emptyset) \to ⋃ ran ((z \in P ⟼ t (z) ∖ ⋂ ran U) \circ Q) \cap ⋂ ran U = \emptyset$
93	77 91 92	mp2an	$⊢ ⋃ ran ((z \in P ⟼ t (z) ∖ ⋂ ran U) \circ Q) \cap ⋂ ran U = \emptyset$
94	75 93	eqtrdi	$⊢ Z = (z \in P ⟼ t (z) ∖ ⋂ ran U) \circ Q \to ⋃ ran Z \cap ⋂ ran U = \emptyset$
95	94	a1d	$⊢ Z = (z \in P ⟼ t (z) ∖ ⋂ ran U) \circ Q \to (Fun t \to ⋃ ran Z \cap ⋂ ran U = \emptyset)$
96	95	adantl	$⊢ (\neg P \in Fin \land Z = (z \in P ⟼ t (z) ∖ ⋂ ran U) \circ Q) \to (Fun t \to ⋃ ran Z \cap ⋂ ran U = \emptyset)$
97	72 96	jaoi	$⊢ ((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 (Fun t \to ⋃ ran Z \cap ⋂ ran U = \emptyset)$
98	6 8 97	mp2b	$⊢ Fun t \to ⋃ ran Z \cap ⋂ ran U = \emptyset$

Metamath Proof Explorer

Theorem fin23lem30

Proof