Metamath Proof Explorer

Theorem 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 ⊢U=seqωi∈ω,u∈V⟼ift⁡i∩u=∅ut⁡i∩u⋃ran⁡t
fin23lem17.f ⊢F=g|∀a∈𝒫gω∀x∈ωa⁡suc⁡x⊆a⁡x→⋂ran⁡a∈ran⁡a
Assertion fin23lem17 ⊢⋃ran⁡t∈F∧t:ω⟶1-1V→⋂ran⁡U∈ran⁡U

Proof

Step Hyp Ref Expression
1 fin23lem.a ⊢U=seqωi∈ω,u∈V⟼ift⁡i∩u=∅ut⁡i∩u⋃ran⁡t
2 fin23lem17.f ⊢F=g|∀a∈𝒫gω∀x∈ωa⁡suc⁡x⊆a⁡x→⋂ran⁡a∈ran⁡a
3 1 fin23lem13 ⊢c∈ω→U⁡suc⁡c⊆U⁡c
4 3 rgen ⊢∀c∈ωU⁡suc⁡c⊆U⁡c
5 fveq1 ⊢b=U→b⁡suc⁡c=U⁡suc⁡c
6 fveq1 ⊢b=U→b⁡c=U⁡c
7 5 6 sseq12d ⊢b=U→b⁡suc⁡c⊆b⁡c↔U⁡suc⁡c⊆U⁡c
8 7 ralbidv ⊢b=U→∀c∈ωb⁡suc⁡c⊆b⁡c↔∀c∈ωU⁡suc⁡c⊆U⁡c
9 rneq ⊢b=U→ran⁡b=ran⁡U
10 9 inteqd ⊢b=U→⋂ran⁡b=⋂ran⁡U
11 10 9 eleq12d ⊢b=U→⋂ran⁡b∈ran⁡b↔⋂ran⁡U∈ran⁡U
12 8 11 imbi12d ⊢b=U→∀c∈ωb⁡suc⁡c⊆b⁡c→⋂ran⁡b∈ran⁡b↔∀c∈ωU⁡suc⁡c⊆U⁡c→⋂ran⁡U∈ran⁡U
13 2 isfin3ds ⊢⋃ran⁡t∈F→⋃ran⁡t∈F↔∀b∈𝒫⋃ran⁡tω∀c∈ωb⁡suc⁡c⊆b⁡c→⋂ran⁡b∈ran⁡b
14 13 ibi ⊢⋃ran⁡t∈F→∀b∈𝒫⋃ran⁡tω∀c∈ωb⁡suc⁡c⊆b⁡c→⋂ran⁡b∈ran⁡b
15 14 adantr ⊢⋃ran⁡t∈F∧t:ω⟶1-1V→∀b∈𝒫⋃ran⁡tω∀c∈ωb⁡suc⁡c⊆b⁡c→⋂ran⁡b∈ran⁡b
16 1 fnseqom ⊢UFnω
17 dffn3 ⊢UFnω↔U:ω⟶ran⁡U
18 16 17 mpbi ⊢U:ω⟶ran⁡U
19 pwuni ⊢ran⁡U⊆𝒫⋃ran⁡U
20 1 fin23lem16 ⊢⋃ran⁡U=⋃ran⁡t
21 20 pweqi ⊢𝒫⋃ran⁡U=𝒫⋃ran⁡t
22 19 21 sseqtri ⊢ran⁡U⊆𝒫⋃ran⁡t
23 fss ⊢U:ω⟶ran⁡U∧ran⁡U⊆𝒫⋃ran⁡t→U:ω⟶𝒫⋃ran⁡t
24 18 22 23 mp2an ⊢U:ω⟶𝒫⋃ran⁡t
25 vex ⊢t∈V
26 25 rnex ⊢ran⁡t∈V
27 26 uniex ⊢⋃ran⁡t∈V
28 27 pwex ⊢𝒫⋃ran⁡t∈V
29 f1f ⊢t:ω⟶1-1V→t:ω⟶V
30 dmfex ⊢t∈V∧t:ω⟶V→ω∈V
31 25 29 30 sylancr ⊢t:ω⟶1-1V→ω∈V
32 31 adantl ⊢⋃ran⁡t∈F∧t:ω⟶1-1V→ω∈V
33 elmapg ⊢𝒫⋃ran⁡t∈V∧ω∈V→U∈𝒫⋃ran⁡tω↔U:ω⟶𝒫⋃ran⁡t
34 28 32 33 sylancr ⊢⋃ran⁡t∈F∧t:ω⟶1-1V→U∈𝒫⋃ran⁡tω↔U:ω⟶𝒫⋃ran⁡t
35 24 34 mpbiri ⊢⋃ran⁡t∈F∧t:ω⟶1-1V→U∈𝒫⋃ran⁡tω
36 12 15 35 rspcdva ⊢⋃ran⁡t∈F∧t:ω⟶1-1V→∀c∈ωU⁡suc⁡c⊆U⁡c→⋂ran⁡U∈ran⁡U
37 4 36 mpi ⊢⋃ran⁡t∈F∧t:ω⟶1-1V→⋂ran⁡U∈ran⁡U