Metamath Proof Explorer

Theorem fin23lem14

Description: Lemma for fin23 . U will never evolve to an empty set if it did not start with one. (Contributed by Stefan O'Rear, 1-Nov-2014)

Ref Expression
Hypothesis fin23lem.a ⊢ 𝑈 = seqω ( ( 𝑖 ∈ ω , 𝑢 ∈ V ↦ if ( ( ( 𝑡 ‘ 𝑖 ) ∩ 𝑢 ) = ∅ , 𝑢 , ( ( 𝑡 ‘ 𝑖 ) ∩ 𝑢 ) ) ) , ∪ ran 𝑡 )
Assertion fin23lem14 ( ( 𝐴 ∈ ω ∧ ∪ ran 𝑡 ≠ ∅ ) → ( 𝑈 ‘ 𝐴 ) ≠ ∅ )

Proof

Step Hyp Ref Expression
1 fin23lem.a ⊢ 𝑈 = seqω ( ( 𝑖 ∈ ω , 𝑢 ∈ V ↦ if ( ( ( 𝑡 ‘ 𝑖 ) ∩ 𝑢 ) = ∅ , 𝑢 , ( ( 𝑡 ‘ 𝑖 ) ∩ 𝑢 ) ) ) , ∪ ran 𝑡 )
2 fveq2 ⊢ ( 𝑎 = ∅ → ( 𝑈 ‘ 𝑎 ) = ( 𝑈 ‘ ∅ ) )
3 2 neeq1d ⊢ ( 𝑎 = ∅ → ( ( 𝑈 ‘ 𝑎 ) ≠ ∅ ↔ ( 𝑈 ‘ ∅ ) ≠ ∅ ) )
4 3 imbi2d ⊢ ( 𝑎 = ∅ → ( ( ∪ ran 𝑡 ≠ ∅ → ( 𝑈 ‘ 𝑎 ) ≠ ∅ ) ↔ ( ∪ ran 𝑡 ≠ ∅ → ( 𝑈 ‘ ∅ ) ≠ ∅ ) ) )
5 fveq2 ⊢ ( 𝑎 = 𝑏 → ( 𝑈 ‘ 𝑎 ) = ( 𝑈 ‘ 𝑏 ) )
6 5 neeq1d ⊢ ( 𝑎 = 𝑏 → ( ( 𝑈 ‘ 𝑎 ) ≠ ∅ ↔ ( 𝑈 ‘ 𝑏 ) ≠ ∅ ) )
7 6 imbi2d ⊢ ( 𝑎 = 𝑏 → ( ( ∪ ran 𝑡 ≠ ∅ → ( 𝑈 ‘ 𝑎 ) ≠ ∅ ) ↔ ( ∪ ran 𝑡 ≠ ∅ → ( 𝑈 ‘ 𝑏 ) ≠ ∅ ) ) )
8 fveq2 ⊢ ( 𝑎 = suc 𝑏 → ( 𝑈 ‘ 𝑎 ) = ( 𝑈 ‘ suc 𝑏 ) )
9 8 neeq1d ⊢ ( 𝑎 = suc 𝑏 → ( ( 𝑈 ‘ 𝑎 ) ≠ ∅ ↔ ( 𝑈 ‘ suc 𝑏 ) ≠ ∅ ) )
10 9 imbi2d ⊢ ( 𝑎 = suc 𝑏 → ( ( ∪ ran 𝑡 ≠ ∅ → ( 𝑈 ‘ 𝑎 ) ≠ ∅ ) ↔ ( ∪ ran 𝑡 ≠ ∅ → ( 𝑈 ‘ suc 𝑏 ) ≠ ∅ ) ) )
11 fveq2 ⊢ ( 𝑎 = 𝐴 → ( 𝑈 ‘ 𝑎 ) = ( 𝑈 ‘ 𝐴 ) )
12 11 neeq1d ⊢ ( 𝑎 = 𝐴 → ( ( 𝑈 ‘ 𝑎 ) ≠ ∅ ↔ ( 𝑈 ‘ 𝐴 ) ≠ ∅ ) )
13 12 imbi2d ⊢ ( 𝑎 = 𝐴 → ( ( ∪ ran 𝑡 ≠ ∅ → ( 𝑈 ‘ 𝑎 ) ≠ ∅ ) ↔ ( ∪ ran 𝑡 ≠ ∅ → ( 𝑈 ‘ 𝐴 ) ≠ ∅ ) ) )
14 vex ⊢ 𝑡 ∈ V
15 14 rnex ⊢ ran 𝑡 ∈ V
16 15 uniex ⊢ ∪ ran 𝑡 ∈ V
17 1 seqom0g ⊢ ( ∪ ran 𝑡 ∈ V → ( 𝑈 ‘ ∅ ) = ∪ ran 𝑡 )
18 16 17 mp1i ⊢ ( ∪ ran 𝑡 ≠ ∅ → ( 𝑈 ‘ ∅ ) = ∪ ran 𝑡 )
19 id ⊢ ( ∪ ran 𝑡 ≠ ∅ → ∪ ran 𝑡 ≠ ∅ )
20 18 19 eqnetrd ⊢ ( ∪ ran 𝑡 ≠ ∅ → ( 𝑈 ‘ ∅ ) ≠ ∅ )
21 1 fin23lem12 ⊢ ( 𝑏 ∈ ω → ( 𝑈 ‘ suc 𝑏 ) = if ( ( ( 𝑡 ‘ 𝑏 ) ∩ ( 𝑈 ‘ 𝑏 ) ) = ∅ , ( 𝑈 ‘ 𝑏 ) , ( ( 𝑡 ‘ 𝑏 ) ∩ ( 𝑈 ‘ 𝑏 ) ) ) )
22 21 adantr ⊢ ( ( 𝑏 ∈ ω ∧ ( 𝑈 ‘ 𝑏 ) ≠ ∅ ) → ( 𝑈 ‘ suc 𝑏 ) = if ( ( ( 𝑡 ‘ 𝑏 ) ∩ ( 𝑈 ‘ 𝑏 ) ) = ∅ , ( 𝑈 ‘ 𝑏 ) , ( ( 𝑡 ‘ 𝑏 ) ∩ ( 𝑈 ‘ 𝑏 ) ) ) )
23 iftrue ⊢ ( ( ( 𝑡 ‘ 𝑏 ) ∩ ( 𝑈 ‘ 𝑏 ) ) = ∅ → if ( ( ( 𝑡 ‘ 𝑏 ) ∩ ( 𝑈 ‘ 𝑏 ) ) = ∅ , ( 𝑈 ‘ 𝑏 ) , ( ( 𝑡 ‘ 𝑏 ) ∩ ( 𝑈 ‘ 𝑏 ) ) ) = ( 𝑈 ‘ 𝑏 ) )
24 23 adantr ⊢ ( ( ( ( 𝑡 ‘ 𝑏 ) ∩ ( 𝑈 ‘ 𝑏 ) ) = ∅ ∧ ( 𝑏 ∈ ω ∧ ( 𝑈 ‘ 𝑏 ) ≠ ∅ ) ) → if ( ( ( 𝑡 ‘ 𝑏 ) ∩ ( 𝑈 ‘ 𝑏 ) ) = ∅ , ( 𝑈 ‘ 𝑏 ) , ( ( 𝑡 ‘ 𝑏 ) ∩ ( 𝑈 ‘ 𝑏 ) ) ) = ( 𝑈 ‘ 𝑏 ) )
25 simprr ⊢ ( ( ( ( 𝑡 ‘ 𝑏 ) ∩ ( 𝑈 ‘ 𝑏 ) ) = ∅ ∧ ( 𝑏 ∈ ω ∧ ( 𝑈 ‘ 𝑏 ) ≠ ∅ ) ) → ( 𝑈 ‘ 𝑏 ) ≠ ∅ )
26 24 25 eqnetrd ⊢ ( ( ( ( 𝑡 ‘ 𝑏 ) ∩ ( 𝑈 ‘ 𝑏 ) ) = ∅ ∧ ( 𝑏 ∈ ω ∧ ( 𝑈 ‘ 𝑏 ) ≠ ∅ ) ) → if ( ( ( 𝑡 ‘ 𝑏 ) ∩ ( 𝑈 ‘ 𝑏 ) ) = ∅ , ( 𝑈 ‘ 𝑏 ) , ( ( 𝑡 ‘ 𝑏 ) ∩ ( 𝑈 ‘ 𝑏 ) ) ) ≠ ∅ )
27 iffalse ⊢ ( ¬ ( ( 𝑡 ‘ 𝑏 ) ∩ ( 𝑈 ‘ 𝑏 ) ) = ∅ → if ( ( ( 𝑡 ‘ 𝑏 ) ∩ ( 𝑈 ‘ 𝑏 ) ) = ∅ , ( 𝑈 ‘ 𝑏 ) , ( ( 𝑡 ‘ 𝑏 ) ∩ ( 𝑈 ‘ 𝑏 ) ) ) = ( ( 𝑡 ‘ 𝑏 ) ∩ ( 𝑈 ‘ 𝑏 ) ) )
28 27 adantr ⊢ ( ( ¬ ( ( 𝑡 ‘ 𝑏 ) ∩ ( 𝑈 ‘ 𝑏 ) ) = ∅ ∧ ( 𝑏 ∈ ω ∧ ( 𝑈 ‘ 𝑏 ) ≠ ∅ ) ) → if ( ( ( 𝑡 ‘ 𝑏 ) ∩ ( 𝑈 ‘ 𝑏 ) ) = ∅ , ( 𝑈 ‘ 𝑏 ) , ( ( 𝑡 ‘ 𝑏 ) ∩ ( 𝑈 ‘ 𝑏 ) ) ) = ( ( 𝑡 ‘ 𝑏 ) ∩ ( 𝑈 ‘ 𝑏 ) ) )
29 neqne ⊢ ( ¬ ( ( 𝑡 ‘ 𝑏 ) ∩ ( 𝑈 ‘ 𝑏 ) ) = ∅ → ( ( 𝑡 ‘ 𝑏 ) ∩ ( 𝑈 ‘ 𝑏 ) ) ≠ ∅ )
30 29 adantr ⊢ ( ( ¬ ( ( 𝑡 ‘ 𝑏 ) ∩ ( 𝑈 ‘ 𝑏 ) ) = ∅ ∧ ( 𝑏 ∈ ω ∧ ( 𝑈 ‘ 𝑏 ) ≠ ∅ ) ) → ( ( 𝑡 ‘ 𝑏 ) ∩ ( 𝑈 ‘ 𝑏 ) ) ≠ ∅ )
31 28 30 eqnetrd ⊢ ( ( ¬ ( ( 𝑡 ‘ 𝑏 ) ∩ ( 𝑈 ‘ 𝑏 ) ) = ∅ ∧ ( 𝑏 ∈ ω ∧ ( 𝑈 ‘ 𝑏 ) ≠ ∅ ) ) → if ( ( ( 𝑡 ‘ 𝑏 ) ∩ ( 𝑈 ‘ 𝑏 ) ) = ∅ , ( 𝑈 ‘ 𝑏 ) , ( ( 𝑡 ‘ 𝑏 ) ∩ ( 𝑈 ‘ 𝑏 ) ) ) ≠ ∅ )
32 26 31 pm2.61ian ⊢ ( ( 𝑏 ∈ ω ∧ ( 𝑈 ‘ 𝑏 ) ≠ ∅ ) → if ( ( ( 𝑡 ‘ 𝑏 ) ∩ ( 𝑈 ‘ 𝑏 ) ) = ∅ , ( 𝑈 ‘ 𝑏 ) , ( ( 𝑡 ‘ 𝑏 ) ∩ ( 𝑈 ‘ 𝑏 ) ) ) ≠ ∅ )
33 22 32 eqnetrd ⊢ ( ( 𝑏 ∈ ω ∧ ( 𝑈 ‘ 𝑏 ) ≠ ∅ ) → ( 𝑈 ‘ suc 𝑏 ) ≠ ∅ )
34 33 ex ⊢ ( 𝑏 ∈ ω → ( ( 𝑈 ‘ 𝑏 ) ≠ ∅ → ( 𝑈 ‘ suc 𝑏 ) ≠ ∅ ) )
35 34 imim2d ⊢ ( 𝑏 ∈ ω → ( ( ∪ ran 𝑡 ≠ ∅ → ( 𝑈 ‘ 𝑏 ) ≠ ∅ ) → ( ∪ ran 𝑡 ≠ ∅ → ( 𝑈 ‘ suc 𝑏 ) ≠ ∅ ) ) )
36 4 7 10 13 20 35 finds ⊢ ( 𝐴 ∈ ω → ( ∪ ran 𝑡 ≠ ∅ → ( 𝑈 ‘ 𝐴 ) ≠ ∅ ) )
37 36 imp ⊢ ( ( 𝐴 ∈ ω ∧ ∪ ran 𝑡 ≠ ∅ ) → ( 𝑈 ‘ 𝐴 ) ≠ ∅ )