fin23lem16

Description: Lemma for fin23 . U ranges over the original set; in particular ran U is a set, although we do not assume here that U is. (Contributed by Stefan O'Rear, 1-Nov-2014)

		Ref	Expression
	Hypothesis	fin23lem.a	$⊢ U = {seq}_{ω} ((i \in ω, u \in V ⟼ if (t (i) \cap u = \emptyset, u, t (i) \cap u)), ⋃ ran t)$
	Assertion	fin23lem16	$⊢ ⋃ ran U = ⋃ 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		unissb	$⊢ ⋃ ran U \subseteq ⋃ ran t \leftrightarrow \forall a \in ran U a \subseteq ⋃ ran t$
3	1	fnseqom	$⊢ U Fn ω$
4		fvelrnb	$⊢ U Fn ω \to (a \in ran U \leftrightarrow \exists b \in ω U (b) = a)$
5	3 4	ax-mp	$⊢ a \in ran U \leftrightarrow \exists b \in ω U (b) = a$
6		peano1	$⊢ \emptyset \in ω$
7		0ss	$⊢ \emptyset \subseteq b$
8	1	fin23lem15	$⊢ ((b \in ω \land \emptyset \in ω) \land \emptyset \subseteq b) \to U (b) \subseteq U (\emptyset)$
9	7 8	mpan2	$⊢ (b \in ω \land \emptyset \in ω) \to U (b) \subseteq U (\emptyset)$
10	6 9	mpan2	$⊢ b \in ω \to U (b) \subseteq U (\emptyset)$
11		vex	$⊢ t \in V$
12	11	rnex	$⊢ ran t \in V$
13	12	uniex	$⊢ ⋃ ran t \in V$
14	1	seqom0g	$⊢ ⋃ ran t \in V \to U (\emptyset) = ⋃ ran t$
15	13 14	ax-mp	$⊢ U (\emptyset) = ⋃ ran t$
16	10 15	sseqtrdi	$⊢ b \in ω \to U (b) \subseteq ⋃ ran t$
17		sseq1	$⊢ U (b) = a \to (U (b) \subseteq ⋃ ran t \leftrightarrow a \subseteq ⋃ ran t)$
18	16 17	syl5ibcom	$⊢ b \in ω \to (U (b) = a \to a \subseteq ⋃ ran t)$
19	18	rexlimiv	$⊢ \exists b \in ω U (b) = a \to a \subseteq ⋃ ran t$
20	5 19	sylbi	$⊢ a \in ran U \to a \subseteq ⋃ ran t$
21	2 20	mprgbir	$⊢ ⋃ ran U \subseteq ⋃ ran t$
22		fnfvelrn	$⊢ (U Fn ω \land \emptyset \in ω) \to U (\emptyset) \in ran U$
23	3 6 22	mp2an	$⊢ U (\emptyset) \in ran U$
24	15 23	eqeltrri	$⊢ ⋃ ran t \in ran U$
25		elssuni	$⊢ ⋃ ran t \in ran U \to ⋃ ran t \subseteq ⋃ ran U$
26	24 25	ax-mp	$⊢ ⋃ ran t \subseteq ⋃ ran U$
27	21 26	eqssi	$⊢ ⋃ ran U = ⋃ ran t$

Metamath Proof Explorer

Theorem fin23lem16

Proof