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