Metamath Proof Explorer

Theorem fin23lem33

Description: Lemma for fin23 . Discharge hypotheses. (Contributed by Stefan O'Rear, 2-Nov-2014)

Ref Expression
Hypothesis fin23lem33.f ⊢ 𝐹 = { 𝑔 ∣ ∀ 𝑎 ∈ ( 𝒫 𝑔 ↑m ω ) ( ∀ 𝑥 ∈ ω ( 𝑎 ‘ suc 𝑥 ) ⊆ ( 𝑎 ‘ 𝑥 ) → ∩ ran 𝑎 ∈ ran 𝑎 ) }
Assertion fin23lem33 ( 𝐺 ∈ 𝐹 → ∃ 𝑓 ∀ 𝑏 ( ( 𝑏 : ω –1-1→ V ∧ ∪ ran 𝑏 ⊆ 𝐺 ) → ( ( 𝑓 ‘ 𝑏 ) : ω –1-1→ V ∧ ∪ ran ( 𝑓 ‘ 𝑏 ) ⊊ ∪ ran 𝑏 ) ) )

Proof

Step Hyp Ref Expression
1 fin23lem33.f ⊢ 𝐹 = { 𝑔 ∣ ∀ 𝑎 ∈ ( 𝒫 𝑔 ↑m ω ) ( ∀ 𝑥 ∈ ω ( 𝑎 ‘ suc 𝑥 ) ⊆ ( 𝑎 ‘ 𝑥 ) → ∩ ran 𝑎 ∈ ran 𝑎 ) }
2 fveq2 ⊢ ( 𝑗 = 𝑐 → ( 𝑒 ‘ 𝑗 ) = ( 𝑒 ‘ 𝑐 ) )
3 2 ineq1d ⊢ ( 𝑗 = 𝑐 → ( ( 𝑒 ‘ 𝑗 ) ∩ 𝑘 ) = ( ( 𝑒 ‘ 𝑐 ) ∩ 𝑘 ) )
4 3 eqeq1d ⊢ ( 𝑗 = 𝑐 → ( ( ( 𝑒 ‘ 𝑗 ) ∩ 𝑘 ) = ∅ ↔ ( ( 𝑒 ‘ 𝑐 ) ∩ 𝑘 ) = ∅ ) )
5 4 3 ifbieq2d ⊢ ( 𝑗 = 𝑐 → if ( ( ( 𝑒 ‘ 𝑗 ) ∩ 𝑘 ) = ∅ , 𝑘 , ( ( 𝑒 ‘ 𝑗 ) ∩ 𝑘 ) ) = if ( ( ( 𝑒 ‘ 𝑐 ) ∩ 𝑘 ) = ∅ , 𝑘 , ( ( 𝑒 ‘ 𝑐 ) ∩ 𝑘 ) ) )
6 ineq2 ⊢ ( 𝑘 = 𝑑 → ( ( 𝑒 ‘ 𝑐 ) ∩ 𝑘 ) = ( ( 𝑒 ‘ 𝑐 ) ∩ 𝑑 ) )
7 6 eqeq1d ⊢ ( 𝑘 = 𝑑 → ( ( ( 𝑒 ‘ 𝑐 ) ∩ 𝑘 ) = ∅ ↔ ( ( 𝑒 ‘ 𝑐 ) ∩ 𝑑 ) = ∅ ) )
8 id ⊢ ( 𝑘 = 𝑑 → 𝑘 = 𝑑 )
9 7 8 6 ifbieq12d ⊢ ( 𝑘 = 𝑑 → if ( ( ( 𝑒 ‘ 𝑐 ) ∩ 𝑘 ) = ∅ , 𝑘 , ( ( 𝑒 ‘ 𝑐 ) ∩ 𝑘 ) ) = if ( ( ( 𝑒 ‘ 𝑐 ) ∩ 𝑑 ) = ∅ , 𝑑 , ( ( 𝑒 ‘ 𝑐 ) ∩ 𝑑 ) ) )
10 5 9 cbvmpov ⊢ ( 𝑗 ∈ ω , 𝑘 ∈ V ↦ if ( ( ( 𝑒 ‘ 𝑗 ) ∩ 𝑘 ) = ∅ , 𝑘 , ( ( 𝑒 ‘ 𝑗 ) ∩ 𝑘 ) ) ) = ( 𝑐 ∈ ω , 𝑑 ∈ V ↦ if ( ( ( 𝑒 ‘ 𝑐 ) ∩ 𝑑 ) = ∅ , 𝑑 , ( ( 𝑒 ‘ 𝑐 ) ∩ 𝑑 ) ) )
11 eqid ⊢ ∪ ran 𝑒 = ∪ ran 𝑒
12 seqomeq12 ⊢ ( ( ( 𝑗 ∈ ω , 𝑘 ∈ V ↦ if ( ( ( 𝑒 ‘ 𝑗 ) ∩ 𝑘 ) = ∅ , 𝑘 , ( ( 𝑒 ‘ 𝑗 ) ∩ 𝑘 ) ) ) = ( 𝑐 ∈ ω , 𝑑 ∈ V ↦ if ( ( ( 𝑒 ‘ 𝑐 ) ∩ 𝑑 ) = ∅ , 𝑑 , ( ( 𝑒 ‘ 𝑐 ) ∩ 𝑑 ) ) ) ∧ ∪ ran 𝑒 = ∪ ran 𝑒 ) → seqω ( ( 𝑗 ∈ ω , 𝑘 ∈ V ↦ if ( ( ( 𝑒 ‘ 𝑗 ) ∩ 𝑘 ) = ∅ , 𝑘 , ( ( 𝑒 ‘ 𝑗 ) ∩ 𝑘 ) ) ) , ∪ ran 𝑒 ) = seqω ( ( 𝑐 ∈ ω , 𝑑 ∈ V ↦ if ( ( ( 𝑒 ‘ 𝑐 ) ∩ 𝑑 ) = ∅ , 𝑑 , ( ( 𝑒 ‘ 𝑐 ) ∩ 𝑑 ) ) ) , ∪ ran 𝑒 ) )
13 10 11 12 mp2an ⊢ seqω ( ( 𝑗 ∈ ω , 𝑘 ∈ V ↦ if ( ( ( 𝑒 ‘ 𝑗 ) ∩ 𝑘 ) = ∅ , 𝑘 , ( ( 𝑒 ‘ 𝑗 ) ∩ 𝑘 ) ) ) , ∪ ran 𝑒 ) = seqω ( ( 𝑐 ∈ ω , 𝑑 ∈ V ↦ if ( ( ( 𝑒 ‘ 𝑐 ) ∩ 𝑑 ) = ∅ , 𝑑 , ( ( 𝑒 ‘ 𝑐 ) ∩ 𝑑 ) ) ) , ∪ ran 𝑒 )
14 fveq2 ⊢ ( 𝑙 = 𝑦 → ( 𝑒 ‘ 𝑙 ) = ( 𝑒 ‘ 𝑦 ) )
15 14 sseq2d ⊢ ( 𝑙 = 𝑦 → ( ∩ ran seqω ( ( 𝑗 ∈ ω , 𝑘 ∈ V ↦ if ( ( ( 𝑒 ‘ 𝑗 ) ∩ 𝑘 ) = ∅ , 𝑘 , ( ( 𝑒 ‘ 𝑗 ) ∩ 𝑘 ) ) ) , ∪ ran 𝑒 ) ⊆ ( 𝑒 ‘ 𝑙 ) ↔ ∩ ran seqω ( ( 𝑗 ∈ ω , 𝑘 ∈ V ↦ if ( ( ( 𝑒 ‘ 𝑗 ) ∩ 𝑘 ) = ∅ , 𝑘 , ( ( 𝑒 ‘ 𝑗 ) ∩ 𝑘 ) ) ) , ∪ ran 𝑒 ) ⊆ ( 𝑒 ‘ 𝑦 ) ) )
16 15 cbvrabv ⊢ { 𝑙 ∈ ω ∣ ∩ ran seqω ( ( 𝑗 ∈ ω , 𝑘 ∈ V ↦ if ( ( ( 𝑒 ‘ 𝑗 ) ∩ 𝑘 ) = ∅ , 𝑘 , ( ( 𝑒 ‘ 𝑗 ) ∩ 𝑘 ) ) ) , ∪ ran 𝑒 ) ⊆ ( 𝑒 ‘ 𝑙 ) } = { 𝑦 ∈ ω ∣ ∩ ran seqω ( ( 𝑗 ∈ ω , 𝑘 ∈ V ↦ if ( ( ( 𝑒 ‘ 𝑗 ) ∩ 𝑘 ) = ∅ , 𝑘 , ( ( 𝑒 ‘ 𝑗 ) ∩ 𝑘 ) ) ) , ∪ ran 𝑒 ) ⊆ ( 𝑒 ‘ 𝑦 ) }
17 eqid ⊢ ( 𝑔 ∈ ω ↦ ( ℩ 𝑥 ∈ { 𝑙 ∈ ω ∣ ∩ ran seqω ( ( 𝑗 ∈ ω , 𝑘 ∈ V ↦ if ( ( ( 𝑒 ‘ 𝑗 ) ∩ 𝑘 ) = ∅ , 𝑘 , ( ( 𝑒 ‘ 𝑗 ) ∩ 𝑘 ) ) ) , ∪ ran 𝑒 ) ⊆ ( 𝑒 ‘ 𝑙 ) } ( 𝑥 ∩ { 𝑙 ∈ ω ∣ ∩ ran seqω ( ( 𝑗 ∈ ω , 𝑘 ∈ V ↦ if ( ( ( 𝑒 ‘ 𝑗 ) ∩ 𝑘 ) = ∅ , 𝑘 , ( ( 𝑒 ‘ 𝑗 ) ∩ 𝑘 ) ) ) , ∪ ran 𝑒 ) ⊆ ( 𝑒 ‘ 𝑙 ) } ) ≈ 𝑔 ) ) = ( 𝑔 ∈ ω ↦ ( ℩ 𝑥 ∈ { 𝑙 ∈ ω ∣ ∩ ran seqω ( ( 𝑗 ∈ ω , 𝑘 ∈ V ↦ if ( ( ( 𝑒 ‘ 𝑗 ) ∩ 𝑘 ) = ∅ , 𝑘 , ( ( 𝑒 ‘ 𝑗 ) ∩ 𝑘 ) ) ) , ∪ ran 𝑒 ) ⊆ ( 𝑒 ‘ 𝑙 ) } ( 𝑥 ∩ { 𝑙 ∈ ω ∣ ∩ ran seqω ( ( 𝑗 ∈ ω , 𝑘 ∈ V ↦ if ( ( ( 𝑒 ‘ 𝑗 ) ∩ 𝑘 ) = ∅ , 𝑘 , ( ( 𝑒 ‘ 𝑗 ) ∩ 𝑘 ) ) ) , ∪ ran 𝑒 ) ⊆ ( 𝑒 ‘ 𝑙 ) } ) ≈ 𝑔 ) )
18 eqid ⊢ ( 𝑔 ∈ ω ↦ ( ℩ 𝑥 ∈ ( ω ∖ { 𝑙 ∈ ω ∣ ∩ ran seqω ( ( 𝑗 ∈ ω , 𝑘 ∈ V ↦ if ( ( ( 𝑒 ‘ 𝑗 ) ∩ 𝑘 ) = ∅ , 𝑘 , ( ( 𝑒 ‘ 𝑗 ) ∩ 𝑘 ) ) ) , ∪ ran 𝑒 ) ⊆ ( 𝑒 ‘ 𝑙 ) } ) ( 𝑥 ∩ ( ω ∖ { 𝑙 ∈ ω ∣ ∩ ran seqω ( ( 𝑗 ∈ ω , 𝑘 ∈ V ↦ if ( ( ( 𝑒 ‘ 𝑗 ) ∩ 𝑘 ) = ∅ , 𝑘 , ( ( 𝑒 ‘ 𝑗 ) ∩ 𝑘 ) ) ) , ∪ ran 𝑒 ) ⊆ ( 𝑒 ‘ 𝑙 ) } ) ) ≈ 𝑔 ) ) = ( 𝑔 ∈ ω ↦ ( ℩ 𝑥 ∈ ( ω ∖ { 𝑙 ∈ ω ∣ ∩ ran seqω ( ( 𝑗 ∈ ω , 𝑘 ∈ V ↦ if ( ( ( 𝑒 ‘ 𝑗 ) ∩ 𝑘 ) = ∅ , 𝑘 , ( ( 𝑒 ‘ 𝑗 ) ∩ 𝑘 ) ) ) , ∪ ran 𝑒 ) ⊆ ( 𝑒 ‘ 𝑙 ) } ) ( 𝑥 ∩ ( ω ∖ { 𝑙 ∈ ω ∣ ∩ ran seqω ( ( 𝑗 ∈ ω , 𝑘 ∈ V ↦ if ( ( ( 𝑒 ‘ 𝑗 ) ∩ 𝑘 ) = ∅ , 𝑘 , ( ( 𝑒 ‘ 𝑗 ) ∩ 𝑘 ) ) ) , ∪ ran 𝑒 ) ⊆ ( 𝑒 ‘ 𝑙 ) } ) ) ≈ 𝑔 ) )
19 eqid ⊢ if ( { 𝑙 ∈ ω ∣ ∩ ran seqω ( ( 𝑗 ∈ ω , 𝑘 ∈ V ↦ if ( ( ( 𝑒 ‘ 𝑗 ) ∩ 𝑘 ) = ∅ , 𝑘 , ( ( 𝑒 ‘ 𝑗 ) ∩ 𝑘 ) ) ) , ∪ ran 𝑒 ) ⊆ ( 𝑒 ‘ 𝑙 ) } ∈ Fin , ( 𝑒 ∘ ( 𝑔 ∈ ω ↦ ( ℩ 𝑥 ∈ ( ω ∖ { 𝑙 ∈ ω ∣ ∩ ran seqω ( ( 𝑗 ∈ ω , 𝑘 ∈ V ↦ if ( ( ( 𝑒 ‘ 𝑗 ) ∩ 𝑘 ) = ∅ , 𝑘 , ( ( 𝑒 ‘ 𝑗 ) ∩ 𝑘 ) ) ) , ∪ ran 𝑒 ) ⊆ ( 𝑒 ‘ 𝑙 ) } ) ( 𝑥 ∩ ( ω ∖ { 𝑙 ∈ ω ∣ ∩ ran seqω ( ( 𝑗 ∈ ω , 𝑘 ∈ V ↦ if ( ( ( 𝑒 ‘ 𝑗 ) ∩ 𝑘 ) = ∅ , 𝑘 , ( ( 𝑒 ‘ 𝑗 ) ∩ 𝑘 ) ) ) , ∪ ran 𝑒 ) ⊆ ( 𝑒 ‘ 𝑙 ) } ) ) ≈ 𝑔 ) ) ) , ( ( 𝑖 ∈ { 𝑙 ∈ ω ∣ ∩ ran seqω ( ( 𝑗 ∈ ω , 𝑘 ∈ V ↦ if ( ( ( 𝑒 ‘ 𝑗 ) ∩ 𝑘 ) = ∅ , 𝑘 , ( ( 𝑒 ‘ 𝑗 ) ∩ 𝑘 ) ) ) , ∪ ran 𝑒 ) ⊆ ( 𝑒 ‘ 𝑙 ) } ↦ ( ( 𝑒 ‘ 𝑖 ) ∖ ∩ ran seqω ( ( 𝑗 ∈ ω , 𝑘 ∈ V ↦ if ( ( ( 𝑒 ‘ 𝑗 ) ∩ 𝑘 ) = ∅ , 𝑘 , ( ( 𝑒 ‘ 𝑗 ) ∩ 𝑘 ) ) ) , ∪ ran 𝑒 ) ) ) ∘ ( 𝑔 ∈ ω ↦ ( ℩ 𝑥 ∈ { 𝑙 ∈ ω ∣ ∩ ran seqω ( ( 𝑗 ∈ ω , 𝑘 ∈ V ↦ if ( ( ( 𝑒 ‘ 𝑗 ) ∩ 𝑘 ) = ∅ , 𝑘 , ( ( 𝑒 ‘ 𝑗 ) ∩ 𝑘 ) ) ) , ∪ ran 𝑒 ) ⊆ ( 𝑒 ‘ 𝑙 ) } ( 𝑥 ∩ { 𝑙 ∈ ω ∣ ∩ ran seqω ( ( 𝑗 ∈ ω , 𝑘 ∈ V ↦ if ( ( ( 𝑒 ‘ 𝑗 ) ∩ 𝑘 ) = ∅ , 𝑘 , ( ( 𝑒 ‘ 𝑗 ) ∩ 𝑘 ) ) ) , ∪ ran 𝑒 ) ⊆ ( 𝑒 ‘ 𝑙 ) } ) ≈ 𝑔 ) ) ) ) = if ( { 𝑙 ∈ ω ∣ ∩ ran seqω ( ( 𝑗 ∈ ω , 𝑘 ∈ V ↦ if ( ( ( 𝑒 ‘ 𝑗 ) ∩ 𝑘 ) = ∅ , 𝑘 , ( ( 𝑒 ‘ 𝑗 ) ∩ 𝑘 ) ) ) , ∪ ran 𝑒 ) ⊆ ( 𝑒 ‘ 𝑙 ) } ∈ Fin , ( 𝑒 ∘ ( 𝑔 ∈ ω ↦ ( ℩ 𝑥 ∈ ( ω ∖ { 𝑙 ∈ ω ∣ ∩ ran seqω ( ( 𝑗 ∈ ω , 𝑘 ∈ V ↦ if ( ( ( 𝑒 ‘ 𝑗 ) ∩ 𝑘 ) = ∅ , 𝑘 , ( ( 𝑒 ‘ 𝑗 ) ∩ 𝑘 ) ) ) , ∪ ran 𝑒 ) ⊆ ( 𝑒 ‘ 𝑙 ) } ) ( 𝑥 ∩ ( ω ∖ { 𝑙 ∈ ω ∣ ∩ ran seqω ( ( 𝑗 ∈ ω , 𝑘 ∈ V ↦ if ( ( ( 𝑒 ‘ 𝑗 ) ∩ 𝑘 ) = ∅ , 𝑘 , ( ( 𝑒 ‘ 𝑗 ) ∩ 𝑘 ) ) ) , ∪ ran 𝑒 ) ⊆ ( 𝑒 ‘ 𝑙 ) } ) ) ≈ 𝑔 ) ) ) , ( ( 𝑖 ∈ { 𝑙 ∈ ω ∣ ∩ ran seqω ( ( 𝑗 ∈ ω , 𝑘 ∈ V ↦ if ( ( ( 𝑒 ‘ 𝑗 ) ∩ 𝑘 ) = ∅ , 𝑘 , ( ( 𝑒 ‘ 𝑗 ) ∩ 𝑘 ) ) ) , ∪ ran 𝑒 ) ⊆ ( 𝑒 ‘ 𝑙 ) } ↦ ( ( 𝑒 ‘ 𝑖 ) ∖ ∩ ran seqω ( ( 𝑗 ∈ ω , 𝑘 ∈ V ↦ if ( ( ( 𝑒 ‘ 𝑗 ) ∩ 𝑘 ) = ∅ , 𝑘 , ( ( 𝑒 ‘ 𝑗 ) ∩ 𝑘 ) ) ) , ∪ ran 𝑒 ) ) ) ∘ ( 𝑔 ∈ ω ↦ ( ℩ 𝑥 ∈ { 𝑙 ∈ ω ∣ ∩ ran seqω ( ( 𝑗 ∈ ω , 𝑘 ∈ V ↦ if ( ( ( 𝑒 ‘ 𝑗 ) ∩ 𝑘 ) = ∅ , 𝑘 , ( ( 𝑒 ‘ 𝑗 ) ∩ 𝑘 ) ) ) , ∪ ran 𝑒 ) ⊆ ( 𝑒 ‘ 𝑙 ) } ( 𝑥 ∩ { 𝑙 ∈ ω ∣ ∩ ran seqω ( ( 𝑗 ∈ ω , 𝑘 ∈ V ↦ if ( ( ( 𝑒 ‘ 𝑗 ) ∩ 𝑘 ) = ∅ , 𝑘 , ( ( 𝑒 ‘ 𝑗 ) ∩ 𝑘 ) ) ) , ∪ ran 𝑒 ) ⊆ ( 𝑒 ‘ 𝑙 ) } ) ≈ 𝑔 ) ) ) )
20 13 1 16 17 18 19 fin23lem32 ⊢ ( 𝐺 ∈ 𝐹 → ∃ 𝑓 ∀ 𝑏 ( ( 𝑏 : ω –1-1→ V ∧ ∪ ran 𝑏 ⊆ 𝐺 ) → ( ( 𝑓 ‘ 𝑏 ) : ω –1-1→ V ∧ ∪ ran ( 𝑓 ‘ 𝑏 ) ⊊ ∪ ran 𝑏 ) ) )