fin23lem31

Description: Lemma for fin23 . The residual is has a strictly smaller range than the previous sequence. This will be iterated to build an unbounded chain. (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	fin23lem31	$⊢ (t : ω \underset{1-1}{⟶} V \land G \in F \land ⋃ ran t \subseteq G) \to ⋃ ran Z \subset ⋃ 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	2	ssfin3ds	$⊢ (G \in F \land ⋃ ran t \subseteq G) \to ⋃ ran t \in F$
8	1 2 3 4 5 6	fin23lem29	$⊢ ⋃ ran Z \subseteq ⋃ ran t$
9	8	a1i	$⊢ (t : ω \underset{1-1}{⟶} V \land ⋃ ran t \in F) \to ⋃ ran Z \subseteq ⋃ ran t$
10	1 2	fin23lem21	$⊢ (⋃ ran t \in F \land t : ω \underset{1-1}{⟶} V) \to ⋂ ran U \neq \emptyset$
11	10	ancoms	$⊢ (t : ω \underset{1-1}{⟶} V \land ⋃ ran t \in F) \to ⋂ ran U \neq \emptyset$
12		n0	$⊢ ⋂ ran U \neq \emptyset \leftrightarrow \exists a a \in ⋂ ran U$
13	11 12	sylib	$⊢ (t : ω \underset{1-1}{⟶} V \land ⋃ ran t \in F) \to \exists a a \in ⋂ ran U$
14	1	fnseqom	$⊢ U Fn ω$
15		fndm	$⊢ U Fn ω \to dom U = ω$
16	14 15	ax-mp	$⊢ dom U = ω$
17		peano1	$⊢ \emptyset \in ω$
18	17	ne0ii	$⊢ ω \neq \emptyset$
19	16 18	eqnetri	$⊢ dom U \neq \emptyset$
20		dm0rn0	$⊢ dom U = \emptyset \leftrightarrow ran U = \emptyset$
21	20	necon3bii	$⊢ dom U \neq \emptyset \leftrightarrow ran U \neq \emptyset$
22	19 21	mpbi	$⊢ ran U \neq \emptyset$
23		intssuni	$⊢ ran U \neq \emptyset \to ⋂ ran U \subseteq ⋃ ran U$
24	22 23	ax-mp	$⊢ ⋂ ran U \subseteq ⋃ ran U$
25	1	fin23lem16	$⊢ ⋃ ran U = ⋃ ran t$
26	24 25	sseqtri	$⊢ ⋂ ran U \subseteq ⋃ ran t$
27	26	sseli	$⊢ a \in ⋂ ran U \to a \in ⋃ ran t$
28		f1fun	$⊢ t : ω \underset{1-1}{⟶} V \to Fun t$
29	28	adantr	$⊢ (t : ω \underset{1-1}{⟶} V \land ⋃ ran t \in F) \to Fun t$
30	1 2 3 4 5 6	fin23lem30	$⊢ Fun t \to ⋃ ran Z \cap ⋂ ran U = \emptyset$
31	29 30	syl	$⊢ (t : ω \underset{1-1}{⟶} V \land ⋃ ran t \in F) \to ⋃ ran Z \cap ⋂ ran U = \emptyset$
32		disj	$⊢ ⋃ ran Z \cap ⋂ ran U = \emptyset \leftrightarrow \forall a \in ⋃ ran Z \neg a \in ⋂ ran U$
33	31 32	sylib	$⊢ (t : ω \underset{1-1}{⟶} V \land ⋃ ran t \in F) \to \forall a \in ⋃ ran Z \neg a \in ⋂ ran U$
34		rsp	$⊢ \forall a \in ⋃ ran Z \neg a \in ⋂ ran U \to (a \in ⋃ ran Z \to \neg a \in ⋂ ran U)$
35	33 34	syl	$⊢ (t : ω \underset{1-1}{⟶} V \land ⋃ ran t \in F) \to (a \in ⋃ ran Z \to \neg a \in ⋂ ran U)$
36	35	con2d	$⊢ (t : ω \underset{1-1}{⟶} V \land ⋃ ran t \in F) \to (a \in ⋂ ran U \to \neg a \in ⋃ ran Z)$
37	36	imp	$⊢ ((t : ω \underset{1-1}{⟶} V \land ⋃ ran t \in F) \land a \in ⋂ ran U) \to \neg a \in ⋃ ran Z$
38		nelne1	$⊢ (a \in ⋃ ran t \land \neg a \in ⋃ ran Z) \to ⋃ ran t \neq ⋃ ran Z$
39	27 37 38	syl2an2	$⊢ ((t : ω \underset{1-1}{⟶} V \land ⋃ ran t \in F) \land a \in ⋂ ran U) \to ⋃ ran t \neq ⋃ ran Z$
40	39	necomd	$⊢ ((t : ω \underset{1-1}{⟶} V \land ⋃ ran t \in F) \land a \in ⋂ ran U) \to ⋃ ran Z \neq ⋃ ran t$
41	13 40	exlimddv	$⊢ (t : ω \underset{1-1}{⟶} V \land ⋃ ran t \in F) \to ⋃ ran Z \neq ⋃ ran t$
42		df-pss	$⊢ ⋃ ran Z \subset ⋃ ran t \leftrightarrow (⋃ ran Z \subseteq ⋃ ran t \land ⋃ ran Z \neq ⋃ ran t)$
43	9 41 42	sylanbrc	$⊢ (t : ω \underset{1-1}{⟶} V \land ⋃ ran t \in F) \to ⋃ ran Z \subset ⋃ ran t$
44	7 43	sylan2	$⊢ (t : ω \underset{1-1}{⟶} V \land (G \in F \land ⋃ ran t \subseteq G)) \to ⋃ ran Z \subset ⋃ ran t$
45	44	3impb	$⊢ (t : ω \underset{1-1}{⟶} V \land G \in F \land ⋃ ran t \subseteq G) \to ⋃ ran Z \subset ⋃ ran t$

Metamath Proof Explorer

Theorem fin23lem31

Proof