fin23lem29

Description: Lemma for fin23 . The residual is built from the same elements as the previous sequence. (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	fin23lem29	$⊢ ⋃ ran Z \subseteq ⋃ ran t$

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		rneq	$⊢ Z = t \circ R \to ran Z = ran (t \circ R)$
10	9	unieqd	$⊢ Z = t \circ R \to ⋃ ran Z = ⋃ ran (t \circ R)$
11		rncoss	$⊢ ran (t \circ R) \subseteq ran t$
12	11	unissi	$⊢ ⋃ ran (t \circ R) \subseteq ⋃ ran t$
13	10 12	eqsstrdi	$⊢ Z = t \circ R \to ⋃ ran Z \subseteq ⋃ ran t$
14	13	adantl	$⊢ (P \in Fin \land Z = t \circ R) \to ⋃ ran Z \subseteq ⋃ ran t$
15		rneq	$⊢ Z = (z \in P ⟼ t (z) ∖ ⋂ ran U) \circ Q \to ran Z = ran ((z \in P ⟼ t (z) ∖ ⋂ ran U) \circ Q)$
16	15	unieqd	$⊢ Z = (z \in P ⟼ t (z) ∖ ⋂ ran U) \circ Q \to ⋃ ran Z = ⋃ ran ((z \in P ⟼ t (z) ∖ ⋂ ran U) \circ Q)$
17		rncoss	$⊢ ran ((z \in P ⟼ t (z) ∖ ⋂ ran U) \circ Q) \subseteq ran (z \in P ⟼ t (z) ∖ ⋂ ran U)$
18	17	unissi	$⊢ ⋃ ran ((z \in P ⟼ t (z) ∖ ⋂ ran U) \circ Q) \subseteq ⋃ ran (z \in P ⟼ t (z) ∖ ⋂ ran U)$
19		unissb	$⊢ ⋃ ran (z \in P ⟼ t (z) ∖ ⋂ ran U) \subseteq ⋃ ran t \leftrightarrow \forall a \in ran (z \in P ⟼ t (z) ∖ ⋂ ran U) a \subseteq ⋃ ran t$
20		abid	$⊢ a \in \{a \| \exists z \in P a = t (z) ∖ ⋂ ran U\} \leftrightarrow \exists z \in P a = t (z) ∖ ⋂ ran U$
21		fvssunirn	$⊢ t (z) \subseteq ⋃ ran t$
22	21	a1i	$⊢ z \in P \to t (z) \subseteq ⋃ ran t$
23	22	ssdifssd	$⊢ z \in P \to t (z) ∖ ⋂ ran U \subseteq ⋃ ran t$
24		sseq1	$⊢ a = t (z) ∖ ⋂ ran U \to (a \subseteq ⋃ ran t \leftrightarrow t (z) ∖ ⋂ ran U \subseteq ⋃ ran t)$
25	23 24	syl5ibrcom	$⊢ z \in P \to (a = t (z) ∖ ⋂ ran U \to a \subseteq ⋃ ran t)$
26	25	rexlimiv	$⊢ \exists z \in P a = t (z) ∖ ⋂ ran U \to a \subseteq ⋃ ran t$
27	20 26	sylbi	$⊢ a \in \{a \| \exists z \in P a = t (z) ∖ ⋂ ran U\} \to a \subseteq ⋃ ran t$
28		eqid	$⊢ (z \in P ⟼ t (z) ∖ ⋂ ran U) = (z \in P ⟼ t (z) ∖ ⋂ ran U)$
29	28	rnmpt	$⊢ ran (z \in P ⟼ t (z) ∖ ⋂ ran U) = \{a \| \exists z \in P a = t (z) ∖ ⋂ ran U\}$
30	27 29	eleq2s	$⊢ a \in ran (z \in P ⟼ t (z) ∖ ⋂ ran U) \to a \subseteq ⋃ ran t$
31	19 30	mprgbir	$⊢ ⋃ ran (z \in P ⟼ t (z) ∖ ⋂ ran U) \subseteq ⋃ ran t$
32	18 31	sstri	$⊢ ⋃ ran ((z \in P ⟼ t (z) ∖ ⋂ ran U) \circ Q) \subseteq ⋃ ran t$
33	16 32	eqsstrdi	$⊢ Z = (z \in P ⟼ t (z) ∖ ⋂ ran U) \circ Q \to ⋃ ran Z \subseteq ⋃ ran t$
34	33	adantl	$⊢ (\neg P \in Fin \land Z = (z \in P ⟼ t (z) ∖ ⋂ ran U) \circ Q) \to ⋃ ran Z \subseteq ⋃ ran t$
35	14 34	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 ⋃ ran Z \subseteq ⋃ ran t$
36	6 8 35	mp2b	$⊢ ⋃ ran Z \subseteq ⋃ ran t$

Metamath Proof Explorer

Theorem fin23lem29

Proof