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	⊢ 𝑈 = seq_ω ( ( 𝑖 ∈ ω , 𝑢 ∈ V ↦ if ( ( ( 𝑡 ‘ 𝑖 ) ∩ 𝑢 ) = ∅ , 𝑢 , ( ( 𝑡 ‘ 𝑖 ) ∩ 𝑢 ) ) ) , ∪ ran 𝑡 )
	Assertion	fin23lem16	⊢ ∪ ran 𝑈 = ∪ ran 𝑡

Proof

Step	Hyp	Ref	Expression
1		fin23lem.a	⊢ 𝑈 = seq_ω ( ( 𝑖 ∈ ω , 𝑢 ∈ V ↦ if ( ( ( 𝑡 ‘ 𝑖 ) ∩ 𝑢 ) = ∅ , 𝑢 , ( ( 𝑡 ‘ 𝑖 ) ∩ 𝑢 ) ) ) , ∪ ran 𝑡 )
2		unissb	⊢ ( ∪ ran 𝑈 ⊆ ∪ ran 𝑡 ↔ ∀ 𝑎 ∈ ran 𝑈 𝑎 ⊆ ∪ ran 𝑡 )
3	1	fnseqom	⊢ 𝑈 Fn ω
4		fvelrnb	⊢ ( 𝑈 Fn ω → ( 𝑎 ∈ ran 𝑈 ↔ ∃ 𝑏 ∈ ω ( 𝑈 ‘ 𝑏 ) = 𝑎 ) )
5	3 4	ax-mp	⊢ ( 𝑎 ∈ ran 𝑈 ↔ ∃ 𝑏 ∈ ω ( 𝑈 ‘ 𝑏 ) = 𝑎 )
6		peano1	⊢ ∅ ∈ ω
7		0ss	⊢ ∅ ⊆ 𝑏
8	1	fin23lem15	⊢ ( ( ( 𝑏 ∈ ω ∧ ∅ ∈ ω ) ∧ ∅ ⊆ 𝑏 ) → ( 𝑈 ‘ 𝑏 ) ⊆ ( 𝑈 ‘ ∅ ) )
9	7 8	mpan2	⊢ ( ( 𝑏 ∈ ω ∧ ∅ ∈ ω ) → ( 𝑈 ‘ 𝑏 ) ⊆ ( 𝑈 ‘ ∅ ) )
10	6 9	mpan2	⊢ ( 𝑏 ∈ ω → ( 𝑈 ‘ 𝑏 ) ⊆ ( 𝑈 ‘ ∅ ) )
11		vex	⊢ 𝑡 ∈ V
12	11	rnex	⊢ ran 𝑡 ∈ V
13	12	uniex	⊢ ∪ ran 𝑡 ∈ V
14	1	seqom0g	⊢ ( ∪ ran 𝑡 ∈ V → ( 𝑈 ‘ ∅ ) = ∪ ran 𝑡 )
15	13 14	ax-mp	⊢ ( 𝑈 ‘ ∅ ) = ∪ ran 𝑡
16	10 15	sseqtrdi	⊢ ( 𝑏 ∈ ω → ( 𝑈 ‘ 𝑏 ) ⊆ ∪ ran 𝑡 )
17		sseq1	⊢ ( ( 𝑈 ‘ 𝑏 ) = 𝑎 → ( ( 𝑈 ‘ 𝑏 ) ⊆ ∪ ran 𝑡 ↔ 𝑎 ⊆ ∪ ran 𝑡 ) )
18	16 17	syl5ibcom	⊢ ( 𝑏 ∈ ω → ( ( 𝑈 ‘ 𝑏 ) = 𝑎 → 𝑎 ⊆ ∪ ran 𝑡 ) )
19	18	rexlimiv	⊢ ( ∃ 𝑏 ∈ ω ( 𝑈 ‘ 𝑏 ) = 𝑎 → 𝑎 ⊆ ∪ ran 𝑡 )
20	5 19	sylbi	⊢ ( 𝑎 ∈ ran 𝑈 → 𝑎 ⊆ ∪ ran 𝑡 )
21	2 20	mprgbir	⊢ ∪ ran 𝑈 ⊆ ∪ ran 𝑡
22		fnfvelrn	⊢ ( ( 𝑈 Fn ω ∧ ∅ ∈ ω ) → ( 𝑈 ‘ ∅ ) ∈ ran 𝑈 )
23	3 6 22	mp2an	⊢ ( 𝑈 ‘ ∅ ) ∈ ran 𝑈
24	15 23	eqeltrri	⊢ ∪ ran 𝑡 ∈ ran 𝑈
25		elssuni	⊢ ( ∪ ran 𝑡 ∈ ran 𝑈 → ∪ ran 𝑡 ⊆ ∪ ran 𝑈 )
26	24 25	ax-mp	⊢ ∪ ran 𝑡 ⊆ ∪ ran 𝑈
27	21 26	eqssi	⊢ ∪ ran 𝑈 = ∪ ran 𝑡

Metamath Proof Explorer

Theorem fin23lem16

Proof