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