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 ⟼ if t ⁡ i ∩ u = ∅ u t ⁡ 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-1 V → ⋂ ran ⁡ U ∈ ran ⁡ U

Proof

Step Hyp Ref Expression
1 fin23lem.a ⊢ U = seq ω i ∈ ω , u ∈ V ⟼ if t ⁡ i ∩ u = ∅ u t ⁡ 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-1 V → ∀ b ∈ 𝒫 ⋃ ran ⁡ t ω ∀ c ∈ ω b ⁡ suc ⁡ c ⊆ b ⁡ c → ⋂ ran ⁡ b ∈ ran ⁡ b
16 1 fnseqom ⊢ U Fn ω
17 dffn3 ⊢ U Fn ω ↔ 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-1 V → t : ω ⟶ V
30 dmfex ⊢ t ∈ V ∧ t : ω ⟶ V → ω ∈ V
31 25 29 30 sylancr ⊢ t : ω ⟶ 1-1 V → ω ∈ V
32 31 adantl ⊢ ⋃ ran ⁡ t ∈ F ∧ t : ω ⟶ 1-1 V → ω ∈ V
33 elmapg ⊢ 𝒫 ⋃ ran ⁡ t ∈ V ∧ ω ∈ V → U ∈ 𝒫 ⋃ ran ⁡ t ω ↔ U : ω ⟶ 𝒫 ⋃ ran ⁡ t
34 28 32 33 sylancr ⊢ ⋃ ran ⁡ t ∈ F ∧ t : ω ⟶ 1-1 V → U ∈ 𝒫 ⋃ ran ⁡ t ω ↔ U : ω ⟶ 𝒫 ⋃ ran ⁡ t
35 24 34 mpbiri ⊢ ⋃ ran ⁡ t ∈ F ∧ t : ω ⟶ 1-1 V → U ∈ 𝒫 ⋃ ran ⁡ t ω
36 12 15 35 rspcdva ⊢ ⋃ ran ⁡ t ∈ F ∧ t : ω ⟶ 1-1 V → ∀ c ∈ ω U ⁡ suc ⁡ c ⊆ U ⁡ c → ⋂ ran ⁡ U ∈ ran ⁡ U
37 4 36 mpi ⊢ ⋃ ran ⁡ t ∈ F ∧ t : ω ⟶ 1-1 V → ⋂ ran ⁡ U ∈ ran ⁡ U