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 𝐵 ) = ( ( 𝑈𝐴 ) ‘ 𝐵 )