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 𝑡 ≠ ∅ ) → ( 𝑈𝐴 ) ≠ ∅ )