Theorem 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	⊢ 𝑈 = seqω ( ( 𝑖 ∈ ω , 𝑢 ∈ V ↦ if ( ( ( 𝑡 ‘ 𝑖 ) ∩ 𝑢 ) = ∅ , 𝑢 , ( ( 𝑡 ‘ 𝑖 ) ∩ 𝑢 ) ) ) , ∪ ran 𝑡 )
	fin23lem17.f	⊢ 𝐹 = { 𝑔 ∣ ∀ 𝑎 ∈ ( 𝒫 𝑔 ↑m ω ) ( ∀ 𝑥 ∈ ω ( 𝑎 ‘ suc 𝑥 ) ⊆ ( 𝑎 ‘ 𝑥 ) → ∩ ran 𝑎 ∈ ran 𝑎 ) }
	fin23lem.b	⊢ 𝑃 = { 𝑣 ∈ ω ∣ ∩ ran 𝑈 ⊆ ( 𝑡 ‘ 𝑣 ) }
	fin23lem.c	⊢ 𝑄 = ( 𝑤 ∈ ω ↦ ( ℩ 𝑥 ∈ 𝑃 ( 𝑥 ∩ 𝑃 ) ≈ 𝑤 ) )
	fin23lem.d	⊢ 𝑅 = ( 𝑤 ∈ ω ↦ ( ℩ 𝑥 ∈ ( ω ∖ 𝑃 ) ( 𝑥 ∩ ( ω ∖ 𝑃 ) ) ≈ 𝑤 ) )
	fin23lem.e	⊢ 𝑍 = if ( 𝑃 ∈ Fin , ( 𝑡 ∘ 𝑅 ) , ( ( 𝑧 ∈ 𝑃 ↦ ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) ) ∘ 𝑄 ) )
Assertion	fin23lem29	⊢ ∪ ran 𝑍 ⊆ ∪ ran 𝑡

Proof

Step	Hyp	Ref	Expression
1		fin23lem.a	⊢ 𝑈 = seqω ( ( 𝑖 ∈ ω , 𝑢 ∈ V ↦ if ( ( ( 𝑡 ‘ 𝑖 ) ∩ 𝑢 ) = ∅ , 𝑢 , ( ( 𝑡 ‘ 𝑖 ) ∩ 𝑢 ) ) ) , ∪ ran 𝑡 )
2		fin23lem17.f	⊢ 𝐹 = { 𝑔 ∣ ∀ 𝑎 ∈ ( 𝒫 𝑔 ↑m ω ) ( ∀ 𝑥 ∈ ω ( 𝑎 ‘ suc 𝑥 ) ⊆ ( 𝑎 ‘ 𝑥 ) → ∩ ran 𝑎 ∈ ran 𝑎 ) }
3		fin23lem.b	⊢ 𝑃 = { 𝑣 ∈ ω ∣ ∩ ran 𝑈 ⊆ ( 𝑡 ‘ 𝑣 ) }
4		fin23lem.c	⊢ 𝑄 = ( 𝑤 ∈ ω ↦ ( ℩ 𝑥 ∈ 𝑃 ( 𝑥 ∩ 𝑃 ) ≈ 𝑤 ) )
5		fin23lem.d	⊢ 𝑅 = ( 𝑤 ∈ ω ↦ ( ℩ 𝑥 ∈ ( ω ∖ 𝑃 ) ( 𝑥 ∩ ( ω ∖ 𝑃 ) ) ≈ 𝑤 ) )
6		fin23lem.e	⊢ 𝑍 = if ( 𝑃 ∈ Fin , ( 𝑡 ∘ 𝑅 ) , ( ( 𝑧 ∈ 𝑃 ↦ ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) ) ∘ 𝑄 ) )
7		eqif	⊢ ( 𝑍 = if ( 𝑃 ∈ Fin , ( 𝑡 ∘ 𝑅 ) , ( ( 𝑧 ∈ 𝑃 ↦ ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) ) ∘ 𝑄 ) ) ↔ ( ( 𝑃 ∈ Fin ∧ 𝑍 = ( 𝑡 ∘ 𝑅 ) ) ∨ ( ¬ 𝑃 ∈ Fin ∧ 𝑍 = ( ( 𝑧 ∈ 𝑃 ↦ ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) ) ∘ 𝑄 ) ) ) )
8	7	biimpi	⊢ ( 𝑍 = if ( 𝑃 ∈ Fin , ( 𝑡 ∘ 𝑅 ) , ( ( 𝑧 ∈ 𝑃 ↦ ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) ) ∘ 𝑄 ) ) → ( ( 𝑃 ∈ Fin ∧ 𝑍 = ( 𝑡 ∘ 𝑅 ) ) ∨ ( ¬ 𝑃 ∈ Fin ∧ 𝑍 = ( ( 𝑧 ∈ 𝑃 ↦ ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) ) ∘ 𝑄 ) ) ) )
9		rneq	⊢ ( 𝑍 = ( 𝑡 ∘ 𝑅 ) → ran 𝑍 = ran ( 𝑡 ∘ 𝑅 ) )
10	9	unieqd	⊢ ( 𝑍 = ( 𝑡 ∘ 𝑅 ) → ∪ ran 𝑍 = ∪ ran ( 𝑡 ∘ 𝑅 ) )
11		rncoss	⊢ ran ( 𝑡 ∘ 𝑅 ) ⊆ ran 𝑡
12	11	unissi	⊢ ∪ ran ( 𝑡 ∘ 𝑅 ) ⊆ ∪ ran 𝑡
13	10 12	eqsstrdi	⊢ ( 𝑍 = ( 𝑡 ∘ 𝑅 ) → ∪ ran 𝑍 ⊆ ∪ ran 𝑡 )
14	13	adantl	⊢ ( ( 𝑃 ∈ Fin ∧ 𝑍 = ( 𝑡 ∘ 𝑅 ) ) → ∪ ran 𝑍 ⊆ ∪ ran 𝑡 )
15		rneq	⊢ ( 𝑍 = ( ( 𝑧 ∈ 𝑃 ↦ ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) ) ∘ 𝑄 ) → ran 𝑍 = ran ( ( 𝑧 ∈ 𝑃 ↦ ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) ) ∘ 𝑄 ) )
16	15	unieqd	⊢ ( 𝑍 = ( ( 𝑧 ∈ 𝑃 ↦ ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) ) ∘ 𝑄 ) → ∪ ran 𝑍 = ∪ ran ( ( 𝑧 ∈ 𝑃 ↦ ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) ) ∘ 𝑄 ) )
17		rncoss	⊢ ran ( ( 𝑧 ∈ 𝑃 ↦ ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) ) ∘ 𝑄 ) ⊆ ran ( 𝑧 ∈ 𝑃 ↦ ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) )
18	17	unissi	⊢ ∪ ran ( ( 𝑧 ∈ 𝑃 ↦ ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) ) ∘ 𝑄 ) ⊆ ∪ ran ( 𝑧 ∈ 𝑃 ↦ ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) )
19		unissb	⊢ ( ∪ ran ( 𝑧 ∈ 𝑃 ↦ ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) ) ⊆ ∪ ran 𝑡 ↔ ∀ 𝑎 ∈ ran ( 𝑧 ∈ 𝑃 ↦ ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) ) 𝑎 ⊆ ∪ ran 𝑡 )
20		abid	⊢ ( 𝑎 ∈ { 𝑎 ∣ ∃ 𝑧 ∈ 𝑃 𝑎 = ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) } ↔ ∃ 𝑧 ∈ 𝑃 𝑎 = ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) )
21		fvssunirn	⊢ ( 𝑡 ‘ 𝑧 ) ⊆ ∪ ran 𝑡
22	21	a1i	⊢ ( 𝑧 ∈ 𝑃 → ( 𝑡 ‘ 𝑧 ) ⊆ ∪ ran 𝑡 )
23	22	ssdifssd	⊢ ( 𝑧 ∈ 𝑃 → ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) ⊆ ∪ ran 𝑡 )
24		sseq1	⊢ ( 𝑎 = ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) → ( 𝑎 ⊆ ∪ ran 𝑡 ↔ ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) ⊆ ∪ ran 𝑡 ) )
25	23 24	syl5ibrcom	⊢ ( 𝑧 ∈ 𝑃 → ( 𝑎 = ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) → 𝑎 ⊆ ∪ ran 𝑡 ) )
26	25	rexlimiv	⊢ ( ∃ 𝑧 ∈ 𝑃 𝑎 = ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) → 𝑎 ⊆ ∪ ran 𝑡 )
27	20 26	sylbi	⊢ ( 𝑎 ∈ { 𝑎 ∣ ∃ 𝑧 ∈ 𝑃 𝑎 = ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) } → 𝑎 ⊆ ∪ ran 𝑡 )
28		eqid	⊢ ( 𝑧 ∈ 𝑃 ↦ ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) ) = ( 𝑧 ∈ 𝑃 ↦ ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) )
29	28	rnmpt	⊢ ran ( 𝑧 ∈ 𝑃 ↦ ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) ) = { 𝑎 ∣ ∃ 𝑧 ∈ 𝑃 𝑎 = ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) }
30	27 29	eleq2s	⊢ ( 𝑎 ∈ ran ( 𝑧 ∈ 𝑃 ↦ ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) ) → 𝑎 ⊆ ∪ ran 𝑡 )
31	19 30	mprgbir	⊢ ∪ ran ( 𝑧 ∈ 𝑃 ↦ ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) ) ⊆ ∪ ran 𝑡
32	18 31	sstri	⊢ ∪ ran ( ( 𝑧 ∈ 𝑃 ↦ ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) ) ∘ 𝑄 ) ⊆ ∪ ran 𝑡
33	16 32	eqsstrdi	⊢ ( 𝑍 = ( ( 𝑧 ∈ 𝑃 ↦ ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) ) ∘ 𝑄 ) → ∪ ran 𝑍 ⊆ ∪ ran 𝑡 )
34	33	adantl	⊢ ( ( ¬ 𝑃 ∈ Fin ∧ 𝑍 = ( ( 𝑧 ∈ 𝑃 ↦ ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) ) ∘ 𝑄 ) ) → ∪ ran 𝑍 ⊆ ∪ ran 𝑡 )
35	14 34	jaoi	⊢ ( ( ( 𝑃 ∈ Fin ∧ 𝑍 = ( 𝑡 ∘ 𝑅 ) ) ∨ ( ¬ 𝑃 ∈ Fin ∧ 𝑍 = ( ( 𝑧 ∈ 𝑃 ↦ ( ( 𝑡 ‘ 𝑧 ) ∖ ∩ ran 𝑈 ) ) ∘ 𝑄 ) ) ) → ∪ ran 𝑍 ⊆ ∪ ran 𝑡 )
36	6 8 35	mp2b	⊢ ∪ ran 𝑍 ⊆ ∪ ran 𝑡