fin23lem21

Description: Lemma for fin23 . X is not empty. We only need here that t has at least one set in its range besides (/) ; the much stronger hypothesis here will serve as our induction hypothesis though. (Contributed by Stefan O'Rear, 1-Nov-2014) (Revised by Mario Carneiro, 6-May-2015)

	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)\}$
Assertion	fin23lem21	$⊢ (⋃ ran t \in F \land t : ω \underset{1-1}{⟶} V) \to ⋂ ran U \neq \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	1 2	fin23lem17	$⊢ (⋃ ran t \in F \land t : ω \underset{1-1}{⟶} V) \to ⋂ ran U \in ran U$
4	1	fnseqom	$⊢ U Fn ω$
5		fvelrnb	$⊢ U Fn ω \to (⋂ ran U \in ran U \leftrightarrow \exists a \in ω U (a) = ⋂ ran U)$
6	4 5	ax-mp	$⊢ ⋂ ran U \in ran U \leftrightarrow \exists a \in ω U (a) = ⋂ ran U$
7		id	$⊢ a \in ω \to a \in ω$
8		vex	$⊢ t \in V$
9		f1f1orn	$⊢ t : ω \underset{1-1}{⟶} V \to t : ω \underset{1-1 onto}{⟶} ran t$
10		f1oen3g	$⊢ (t \in V \land t : ω \underset{1-1 onto}{⟶} ran t) \to ω \approx ran t$
11	8 9 10	sylancr	$⊢ t : ω \underset{1-1}{⟶} V \to ω \approx ran t$
12		ominf	$⊢ \neg ω \in Fin$
13		ssdif0	$⊢ ran t \subseteq \{\emptyset\} \leftrightarrow ran t ∖ \{\emptyset\} = \emptyset$
14		snfi	$⊢ \{\emptyset\} \in Fin$
15		ssfi	$⊢ (\{\emptyset\} \in Fin \land ran t \subseteq \{\emptyset\}) \to ran t \in Fin$
16	14 15	mpan	$⊢ ran t \subseteq \{\emptyset\} \to ran t \in Fin$
17		enfi	$⊢ ω \approx ran t \to (ω \in Fin \leftrightarrow ran t \in Fin)$
18	16 17	imbitrrid	$⊢ ω \approx ran t \to (ran t \subseteq \{\emptyset\} \to ω \in Fin)$
19	13 18	biimtrrid	$⊢ ω \approx ran t \to (ran t ∖ \{\emptyset\} = \emptyset \to ω \in Fin)$
20	19	necon3bd	$⊢ ω \approx ran t \to (\neg ω \in Fin \to ran t ∖ \{\emptyset\} \neq \emptyset)$
21	11 12 20	mpisyl	$⊢ t : ω \underset{1-1}{⟶} V \to ran t ∖ \{\emptyset\} \neq \emptyset$
22		n0	$⊢ ran t ∖ \{\emptyset\} \neq \emptyset \leftrightarrow \exists a a \in (ran t ∖ \{\emptyset\})$
23		eldifsn	$⊢ a \in (ran t ∖ \{\emptyset\}) \leftrightarrow (a \in ran t \land a \neq \emptyset)$
24		elssuni	$⊢ a \in ran t \to a \subseteq ⋃ ran t$
25		ssn0	$⊢ (a \subseteq ⋃ ran t \land a \neq \emptyset) \to ⋃ ran t \neq \emptyset$
26	24 25	sylan	$⊢ (a \in ran t \land a \neq \emptyset) \to ⋃ ran t \neq \emptyset$
27	23 26	sylbi	$⊢ a \in (ran t ∖ \{\emptyset\}) \to ⋃ ran t \neq \emptyset$
28	27	exlimiv	$⊢ \exists a a \in (ran t ∖ \{\emptyset\}) \to ⋃ ran t \neq \emptyset$
29	22 28	sylbi	$⊢ ran t ∖ \{\emptyset\} \neq \emptyset \to ⋃ ran t \neq \emptyset$
30	21 29	syl	$⊢ t : ω \underset{1-1}{⟶} V \to ⋃ ran t \neq \emptyset$
31	1	fin23lem14	$⊢ (a \in ω \land ⋃ ran t \neq \emptyset) \to U (a) \neq \emptyset$
32	7 30 31	syl2anr	$⊢ (t : ω \underset{1-1}{⟶} V \land a \in ω) \to U (a) \neq \emptyset$
33		neeq1	$⊢ U (a) = ⋂ ran U \to (U (a) \neq \emptyset \leftrightarrow ⋂ ran U \neq \emptyset)$
34	32 33	syl5ibcom	$⊢ (t : ω \underset{1-1}{⟶} V \land a \in ω) \to (U (a) = ⋂ ran U \to ⋂ ran U \neq \emptyset)$
35	34	rexlimdva	$⊢ t : ω \underset{1-1}{⟶} V \to (\exists a \in ω U (a) = ⋂ ran U \to ⋂ ran U \neq \emptyset)$
36	6 35	biimtrid	$⊢ t : ω \underset{1-1}{⟶} V \to (⋂ ran U \in ran U \to ⋂ ran U \neq \emptyset)$
37	36	adantl	$⊢ (⋃ ran t \in F \land t : ω \underset{1-1}{⟶} V) \to (⋂ ran U \in ran U \to ⋂ ran U \neq \emptyset)$
38	3 37	mpd	$⊢ (⋃ ran t \in F \land t : ω \underset{1-1}{⟶} V) \to ⋂ ran U \neq \emptyset$

Metamath Proof Explorer

Theorem fin23lem21

Proof