fin23lem17

Description: Lemma for fin23 . By ? Fin3DS ? , U achieves its minimum ( X in the synopsis above, but we will not be assigning a symbol here). TODO: Fix comment; math symbol Fin3DS does not exist. (Contributed by Stefan O'Rear, 4-Nov-2014) (Revised by Mario Carneiro, 17-May-2015)

	Ref	Expression
Hypotheses	fin23lem.a	⊢ 𝑈 = seq_ω ( ( 𝑖 ∈ ω , 𝑢 ∈ V ↦ if ( ( ( 𝑡 ‘ 𝑖 ) ∩ 𝑢 ) = ∅ , 𝑢 , ( ( 𝑡 ‘ 𝑖 ) ∩ 𝑢 ) ) ) , ∪ ran 𝑡 )
	fin23lem17.f	⊢ 𝐹 = { 𝑔 ∣ ∀ 𝑎 ∈ ( 𝒫 𝑔 ↑_m ω ) ( ∀ 𝑥 ∈ ω ( 𝑎 ‘ suc 𝑥 ) ⊆ ( 𝑎 ‘ 𝑥 ) → ∩ ran 𝑎 ∈ ran 𝑎 ) }
Assertion	fin23lem17	⊢ ( ( ∪ ran 𝑡 ∈ 𝐹 ∧ 𝑡 : ω –1-1→ 𝑉 ) → ∩ ran 𝑈 ∈ ran 𝑈 )

Proof

Step	Hyp	Ref	Expression
1		fin23lem.a	⊢ 𝑈 = seq_ω ( ( 𝑖 ∈ ω , 𝑢 ∈ V ↦ if ( ( ( 𝑡 ‘ 𝑖 ) ∩ 𝑢 ) = ∅ , 𝑢 , ( ( 𝑡 ‘ 𝑖 ) ∩ 𝑢 ) ) ) , ∪ ran 𝑡 )
2		fin23lem17.f	⊢ 𝐹 = { 𝑔 ∣ ∀ 𝑎 ∈ ( 𝒫 𝑔 ↑_m ω ) ( ∀ 𝑥 ∈ ω ( 𝑎 ‘ suc 𝑥 ) ⊆ ( 𝑎 ‘ 𝑥 ) → ∩ ran 𝑎 ∈ ran 𝑎 ) }
3	1	fin23lem13	⊢ ( 𝑐 ∈ ω → ( 𝑈 ‘ suc 𝑐 ) ⊆ ( 𝑈 ‘ 𝑐 ) )
4	3	rgen	⊢ ∀ 𝑐 ∈ ω ( 𝑈 ‘ suc 𝑐 ) ⊆ ( 𝑈 ‘ 𝑐 )
5		fveq1	⊢ ( 𝑏 = 𝑈 → ( 𝑏 ‘ suc 𝑐 ) = ( 𝑈 ‘ suc 𝑐 ) )
6		fveq1	⊢ ( 𝑏 = 𝑈 → ( 𝑏 ‘ 𝑐 ) = ( 𝑈 ‘ 𝑐 ) )
7	5 6	sseq12d	⊢ ( 𝑏 = 𝑈 → ( ( 𝑏 ‘ suc 𝑐 ) ⊆ ( 𝑏 ‘ 𝑐 ) ↔ ( 𝑈 ‘ suc 𝑐 ) ⊆ ( 𝑈 ‘ 𝑐 ) ) )
8	7	ralbidv	⊢ ( 𝑏 = 𝑈 → ( ∀ 𝑐 ∈ ω ( 𝑏 ‘ suc 𝑐 ) ⊆ ( 𝑏 ‘ 𝑐 ) ↔ ∀ 𝑐 ∈ ω ( 𝑈 ‘ suc 𝑐 ) ⊆ ( 𝑈 ‘ 𝑐 ) ) )
9		rneq	⊢ ( 𝑏 = 𝑈 → ran 𝑏 = ran 𝑈 )
10	9	inteqd	⊢ ( 𝑏 = 𝑈 → ∩ ran 𝑏 = ∩ ran 𝑈 )
11	10 9	eleq12d	⊢ ( 𝑏 = 𝑈 → ( ∩ ran 𝑏 ∈ ran 𝑏 ↔ ∩ ran 𝑈 ∈ ran 𝑈 ) )
12	8 11	imbi12d	⊢ ( 𝑏 = 𝑈 → ( ( ∀ 𝑐 ∈ ω ( 𝑏 ‘ suc 𝑐 ) ⊆ ( 𝑏 ‘ 𝑐 ) → ∩ ran 𝑏 ∈ ran 𝑏 ) ↔ ( ∀ 𝑐 ∈ ω ( 𝑈 ‘ suc 𝑐 ) ⊆ ( 𝑈 ‘ 𝑐 ) → ∩ ran 𝑈 ∈ ran 𝑈 ) ) )
13	2	isfin3ds	⊢ ( ∪ ran 𝑡 ∈ 𝐹 → ( ∪ ran 𝑡 ∈ 𝐹 ↔ ∀ 𝑏 ∈ ( 𝒫 ∪ ran 𝑡 ↑_m ω ) ( ∀ 𝑐 ∈ ω ( 𝑏 ‘ suc 𝑐 ) ⊆ ( 𝑏 ‘ 𝑐 ) → ∩ ran 𝑏 ∈ ran 𝑏 ) ) )
14	13	ibi	⊢ ( ∪ ran 𝑡 ∈ 𝐹 → ∀ 𝑏 ∈ ( 𝒫 ∪ ran 𝑡 ↑_m ω ) ( ∀ 𝑐 ∈ ω ( 𝑏 ‘ suc 𝑐 ) ⊆ ( 𝑏 ‘ 𝑐 ) → ∩ ran 𝑏 ∈ ran 𝑏 ) )
15	14	adantr	⊢ ( ( ∪ ran 𝑡 ∈ 𝐹 ∧ 𝑡 : ω –1-1→ 𝑉 ) → ∀ 𝑏 ∈ ( 𝒫 ∪ ran 𝑡 ↑_m ω ) ( ∀ 𝑐 ∈ ω ( 𝑏 ‘ suc 𝑐 ) ⊆ ( 𝑏 ‘ 𝑐 ) → ∩ ran 𝑏 ∈ ran 𝑏 ) )
16	1	fnseqom	⊢ 𝑈 Fn ω
17		dffn3	⊢ ( 𝑈 Fn ω ↔ 𝑈 : ω ⟶ ran 𝑈 )
18	16 17	mpbi	⊢ 𝑈 : ω ⟶ ran 𝑈
19		pwuni	⊢ ran 𝑈 ⊆ 𝒫 ∪ ran 𝑈
20	1	fin23lem16	⊢ ∪ ran 𝑈 = ∪ ran 𝑡
21	20	pweqi	⊢ 𝒫 ∪ ran 𝑈 = 𝒫 ∪ ran 𝑡
22	19 21	sseqtri	⊢ ran 𝑈 ⊆ 𝒫 ∪ ran 𝑡
23		fss	⊢ ( ( 𝑈 : ω ⟶ ran 𝑈 ∧ ran 𝑈 ⊆ 𝒫 ∪ ran 𝑡 ) → 𝑈 : ω ⟶ 𝒫 ∪ ran 𝑡 )
24	18 22 23	mp2an	⊢ 𝑈 : ω ⟶ 𝒫 ∪ ran 𝑡
25		vex	⊢ 𝑡 ∈ V
26	25	rnex	⊢ ran 𝑡 ∈ V
27	26	uniex	⊢ ∪ ran 𝑡 ∈ V
28	27	pwex	⊢ 𝒫 ∪ ran 𝑡 ∈ V
29		f1f	⊢ ( 𝑡 : ω –1-1→ 𝑉 → 𝑡 : ω ⟶ 𝑉 )
30		dmfex	⊢ ( ( 𝑡 ∈ V ∧ 𝑡 : ω ⟶ 𝑉 ) → ω ∈ V )
31	25 29 30	sylancr	⊢ ( 𝑡 : ω –1-1→ 𝑉 → ω ∈ V )
32	31	adantl	⊢ ( ( ∪ ran 𝑡 ∈ 𝐹 ∧ 𝑡 : ω –1-1→ 𝑉 ) → ω ∈ V )
33		elmapg	⊢ ( ( 𝒫 ∪ ran 𝑡 ∈ V ∧ ω ∈ V ) → ( 𝑈 ∈ ( 𝒫 ∪ ran 𝑡 ↑_m ω ) ↔ 𝑈 : ω ⟶ 𝒫 ∪ ran 𝑡 ) )
34	28 32 33	sylancr	⊢ ( ( ∪ ran 𝑡 ∈ 𝐹 ∧ 𝑡 : ω –1-1→ 𝑉 ) → ( 𝑈 ∈ ( 𝒫 ∪ ran 𝑡 ↑_m ω ) ↔ 𝑈 : ω ⟶ 𝒫 ∪ ran 𝑡 ) )
35	24 34	mpbiri	⊢ ( ( ∪ ran 𝑡 ∈ 𝐹 ∧ 𝑡 : ω –1-1→ 𝑉 ) → 𝑈 ∈ ( 𝒫 ∪ ran 𝑡 ↑_m ω ) )
36	12 15 35	rspcdva	⊢ ( ( ∪ ran 𝑡 ∈ 𝐹 ∧ 𝑡 : ω –1-1→ 𝑉 ) → ( ∀ 𝑐 ∈ ω ( 𝑈 ‘ suc 𝑐 ) ⊆ ( 𝑈 ‘ 𝑐 ) → ∩ ran 𝑈 ∈ ran 𝑈 ) )
37	4 36	mpi	⊢ ( ( ∪ ran 𝑡 ∈ 𝐹 ∧ 𝑡 : ω –1-1→ 𝑉 ) → ∩ ran 𝑈 ∈ ran 𝑈 )

Metamath Proof Explorer

Theorem fin23lem17

Proof