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 ⊢ 𝑈 = 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 𝑈 )