Metamath Proof Explorer

Theorem itunisuc

Description: Successor iterated union. (Contributed by Stefan O'Rear, 11-Feb-2015)

Ref Expression
Hypothesis ituni.u ⊢ 𝑈 = ( 𝑥 ∈ V ↦ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , 𝑥 ) ↾ ω ) )
Assertion itunisuc ( ( 𝑈 ‘ 𝐴 ) ‘ suc 𝐵 ) = ∪ ( ( 𝑈 ‘ 𝐴 ) ‘ 𝐵 )

Proof

Step Hyp Ref Expression
1 ituni.u ⊢ 𝑈 = ( 𝑥 ∈ V ↦ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , 𝑥 ) ↾ ω ) )
2 frsuc ⊢ ( 𝐵 ∈ ω → ( ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , 𝐴 ) ↾ ω ) ‘ suc 𝐵 ) = ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) ‘ ( ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , 𝐴 ) ↾ ω ) ‘ 𝐵 ) ) )
3 fvex ⊢ ( ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , 𝐴 ) ↾ ω ) ‘ 𝐵 ) ∈ V
4 unieq ⊢ ( 𝑎 = ( ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , 𝐴 ) ↾ ω ) ‘ 𝐵 ) → ∪ 𝑎 = ∪ ( ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , 𝐴 ) ↾ ω ) ‘ 𝐵 ) )
5 unieq ⊢ ( 𝑦 = 𝑎 → ∪ 𝑦 = ∪ 𝑎 )
6 5 cbvmptv ⊢ ( 𝑦 ∈ V ↦ ∪ 𝑦 ) = ( 𝑎 ∈ V ↦ ∪ 𝑎 )
7 3 uniex ⊢ ∪ ( ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , 𝐴 ) ↾ ω ) ‘ 𝐵 ) ∈ V
8 4 6 7 fvmpt ⊢ ( ( ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , 𝐴 ) ↾ ω ) ‘ 𝐵 ) ∈ V → ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) ‘ ( ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , 𝐴 ) ↾ ω ) ‘ 𝐵 ) ) = ∪ ( ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , 𝐴 ) ↾ ω ) ‘ 𝐵 ) )
9 3 8 ax-mp ⊢ ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) ‘ ( ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , 𝐴 ) ↾ ω ) ‘ 𝐵 ) ) = ∪ ( ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , 𝐴 ) ↾ ω ) ‘ 𝐵 )
10 2 9 eqtrdi ⊢ ( 𝐵 ∈ ω → ( ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , 𝐴 ) ↾ ω ) ‘ suc 𝐵 ) = ∪ ( ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , 𝐴 ) ↾ ω ) ‘ 𝐵 ) )
11 10 adantl ⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ ω ) → ( ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , 𝐴 ) ↾ ω ) ‘ suc 𝐵 ) = ∪ ( ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , 𝐴 ) ↾ ω ) ‘ 𝐵 ) )
12 1 itunifval ⊢ ( 𝐴 ∈ V → ( 𝑈 ‘ 𝐴 ) = ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , 𝐴 ) ↾ ω ) )
13 12 fveq1d ⊢ ( 𝐴 ∈ V → ( ( 𝑈 ‘ 𝐴 ) ‘ suc 𝐵 ) = ( ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , 𝐴 ) ↾ ω ) ‘ suc 𝐵 ) )
14 13 adantr ⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ ω ) → ( ( 𝑈 ‘ 𝐴 ) ‘ suc 𝐵 ) = ( ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , 𝐴 ) ↾ ω ) ‘ suc 𝐵 ) )
15 12 fveq1d ⊢ ( 𝐴 ∈ V → ( ( 𝑈 ‘ 𝐴 ) ‘ 𝐵 ) = ( ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , 𝐴 ) ↾ ω ) ‘ 𝐵 ) )
16 15 adantr ⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ ω ) → ( ( 𝑈 ‘ 𝐴 ) ‘ 𝐵 ) = ( ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , 𝐴 ) ↾ ω ) ‘ 𝐵 ) )
17 16 unieqd ⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ ω ) → ∪ ( ( 𝑈 ‘ 𝐴 ) ‘ 𝐵 ) = ∪ ( ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , 𝐴 ) ↾ ω ) ‘ 𝐵 ) )
18 11 14 17 3eqtr4d ⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ ω ) → ( ( 𝑈 ‘ 𝐴 ) ‘ suc 𝐵 ) = ∪ ( ( 𝑈 ‘ 𝐴 ) ‘ 𝐵 ) )
19 uni0 ⊢ ∪ ∅ = ∅
20 19 eqcomi ⊢ ∅ = ∪ ∅
21 1 itunifn ⊢ ( 𝐴 ∈ V → ( 𝑈 ‘ 𝐴 ) Fn ω )
22 21 fndmd ⊢ ( 𝐴 ∈ V → dom ( 𝑈 ‘ 𝐴 ) = ω )
23 22 eleq2d ⊢ ( 𝐴 ∈ V → ( suc 𝐵 ∈ dom ( 𝑈 ‘ 𝐴 ) ↔ suc 𝐵 ∈ ω ) )
24 peano2b ⊢ ( 𝐵 ∈ ω ↔ suc 𝐵 ∈ ω )
25 23 24 bitr4di ⊢ ( 𝐴 ∈ V → ( suc 𝐵 ∈ dom ( 𝑈 ‘ 𝐴 ) ↔ 𝐵 ∈ ω ) )
26 25 notbid ⊢ ( 𝐴 ∈ V → ( ¬ suc 𝐵 ∈ dom ( 𝑈 ‘ 𝐴 ) ↔ ¬ 𝐵 ∈ ω ) )
27 26 biimpar ⊢ ( ( 𝐴 ∈ V ∧ ¬ 𝐵 ∈ ω ) → ¬ suc 𝐵 ∈ dom ( 𝑈 ‘ 𝐴 ) )
28 ndmfv ⊢ ( ¬ suc 𝐵 ∈ dom ( 𝑈 ‘ 𝐴 ) → ( ( 𝑈 ‘ 𝐴 ) ‘ suc 𝐵 ) = ∅ )
29 27 28 syl ⊢ ( ( 𝐴 ∈ V ∧ ¬ 𝐵 ∈ ω ) → ( ( 𝑈 ‘ 𝐴 ) ‘ suc 𝐵 ) = ∅ )
30 22 eleq2d ⊢ ( 𝐴 ∈ V → ( 𝐵 ∈ dom ( 𝑈 ‘ 𝐴 ) ↔ 𝐵 ∈ ω ) )
31 30 notbid ⊢ ( 𝐴 ∈ V → ( ¬ 𝐵 ∈ dom ( 𝑈 ‘ 𝐴 ) ↔ ¬ 𝐵 ∈ ω ) )
32 31 biimpar ⊢ ( ( 𝐴 ∈ V ∧ ¬ 𝐵 ∈ ω ) → ¬ 𝐵 ∈ dom ( 𝑈 ‘ 𝐴 ) )
33 ndmfv ⊢ ( ¬ 𝐵 ∈ dom ( 𝑈 ‘ 𝐴 ) → ( ( 𝑈 ‘ 𝐴 ) ‘ 𝐵 ) = ∅ )
34 32 33 syl ⊢ ( ( 𝐴 ∈ V ∧ ¬ 𝐵 ∈ ω ) → ( ( 𝑈 ‘ 𝐴 ) ‘ 𝐵 ) = ∅ )
35 34 unieqd ⊢ ( ( 𝐴 ∈ V ∧ ¬ 𝐵 ∈ ω ) → ∪ ( ( 𝑈 ‘ 𝐴 ) ‘ 𝐵 ) = ∪ ∅ )
36 20 29 35 3eqtr4a ⊢ ( ( 𝐴 ∈ V ∧ ¬ 𝐵 ∈ ω ) → ( ( 𝑈 ‘ 𝐴 ) ‘ suc 𝐵 ) = ∪ ( ( 𝑈 ‘ 𝐴 ) ‘ 𝐵 ) )
37 18 36 pm2.61dan ⊢ ( 𝐴 ∈ V → ( ( 𝑈 ‘ 𝐴 ) ‘ suc 𝐵 ) = ∪ ( ( 𝑈 ‘ 𝐴 ) ‘ 𝐵 ) )
38 0fv ⊢ ( ∅ ‘ 𝐵 ) = ∅
39 38 unieqi ⊢ ∪ ( ∅ ‘ 𝐵 ) = ∪ ∅
40 0fv ⊢ ( ∅ ‘ suc 𝐵 ) = ∅
41 19 39 40 3eqtr4ri ⊢ ( ∅ ‘ suc 𝐵 ) = ∪ ( ∅ ‘ 𝐵 )
42 fvprc ⊢ ( ¬ 𝐴 ∈ V → ( 𝑈 ‘ 𝐴 ) = ∅ )
43 42 fveq1d ⊢ ( ¬ 𝐴 ∈ V → ( ( 𝑈 ‘ 𝐴 ) ‘ suc 𝐵 ) = ( ∅ ‘ suc 𝐵 ) )
44 42 fveq1d ⊢ ( ¬ 𝐴 ∈ V → ( ( 𝑈 ‘ 𝐴 ) ‘ 𝐵 ) = ( ∅ ‘ 𝐵 ) )
45 44 unieqd ⊢ ( ¬ 𝐴 ∈ V → ∪ ( ( 𝑈 ‘ 𝐴 ) ‘ 𝐵 ) = ∪ ( ∅ ‘ 𝐵 ) )
46 41 43 45 3eqtr4a ⊢ ( ¬ 𝐴 ∈ V → ( ( 𝑈 ‘ 𝐴 ) ‘ suc 𝐵 ) = ∪ ( ( 𝑈 ‘ 𝐴 ) ‘ 𝐵 ) )
47 37 46 pm2.61i ⊢ ( ( 𝑈 ‘ 𝐴 ) ‘ suc 𝐵 ) = ∪ ( ( 𝑈 ‘ 𝐴 ) ‘ 𝐵 )