Metamath Proof Explorer

Theorem ituniiun

Description: Unwrap an iterated union from the "other end". (Contributed by Stefan O'Rear, 11-Feb-2015)

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

Proof

Step Hyp Ref Expression
1 ituni.u ⊢ 𝑈 = ( 𝑥 ∈ V ↦ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , 𝑥 ) ↾ ω ) )
2 fveq2 ⊢ ( 𝑏 = 𝐴 → ( 𝑈 ‘ 𝑏 ) = ( 𝑈 ‘ 𝐴 ) )
3 2 fveq1d ⊢ ( 𝑏 = 𝐴 → ( ( 𝑈 ‘ 𝑏 ) ‘ suc 𝐵 ) = ( ( 𝑈 ‘ 𝐴 ) ‘ suc 𝐵 ) )
4 iuneq1 ⊢ ( 𝑏 = 𝐴 → ∪ 𝑎 ∈ 𝑏 ( ( 𝑈 ‘ 𝑎 ) ‘ 𝐵 ) = ∪ 𝑎 ∈ 𝐴 ( ( 𝑈 ‘ 𝑎 ) ‘ 𝐵 ) )
5 3 4 eqeq12d ⊢ ( 𝑏 = 𝐴 → ( ( ( 𝑈 ‘ 𝑏 ) ‘ suc 𝐵 ) = ∪ 𝑎 ∈ 𝑏 ( ( 𝑈 ‘ 𝑎 ) ‘ 𝐵 ) ↔ ( ( 𝑈 ‘ 𝐴 ) ‘ suc 𝐵 ) = ∪ 𝑎 ∈ 𝐴 ( ( 𝑈 ‘ 𝑎 ) ‘ 𝐵 ) ) )
6 suceq ⊢ ( 𝑑 = ∅ → suc 𝑑 = suc ∅ )
7 6 fveq2d ⊢ ( 𝑑 = ∅ → ( ( 𝑈 ‘ 𝑏 ) ‘ suc 𝑑 ) = ( ( 𝑈 ‘ 𝑏 ) ‘ suc ∅ ) )
8 fveq2 ⊢ ( 𝑑 = ∅ → ( ( 𝑈 ‘ 𝑎 ) ‘ 𝑑 ) = ( ( 𝑈 ‘ 𝑎 ) ‘ ∅ ) )
9 8 iuneq2d ⊢ ( 𝑑 = ∅ → ∪ 𝑎 ∈ 𝑏 ( ( 𝑈 ‘ 𝑎 ) ‘ 𝑑 ) = ∪ 𝑎 ∈ 𝑏 ( ( 𝑈 ‘ 𝑎 ) ‘ ∅ ) )
10 7 9 eqeq12d ⊢ ( 𝑑 = ∅ → ( ( ( 𝑈 ‘ 𝑏 ) ‘ suc 𝑑 ) = ∪ 𝑎 ∈ 𝑏 ( ( 𝑈 ‘ 𝑎 ) ‘ 𝑑 ) ↔ ( ( 𝑈 ‘ 𝑏 ) ‘ suc ∅ ) = ∪ 𝑎 ∈ 𝑏 ( ( 𝑈 ‘ 𝑎 ) ‘ ∅ ) ) )
11 suceq ⊢ ( 𝑑 = 𝑐 → suc 𝑑 = suc 𝑐 )
12 11 fveq2d ⊢ ( 𝑑 = 𝑐 → ( ( 𝑈 ‘ 𝑏 ) ‘ suc 𝑑 ) = ( ( 𝑈 ‘ 𝑏 ) ‘ suc 𝑐 ) )
13 fveq2 ⊢ ( 𝑑 = 𝑐 → ( ( 𝑈 ‘ 𝑎 ) ‘ 𝑑 ) = ( ( 𝑈 ‘ 𝑎 ) ‘ 𝑐 ) )
14 13 iuneq2d ⊢ ( 𝑑 = 𝑐 → ∪ 𝑎 ∈ 𝑏 ( ( 𝑈 ‘ 𝑎 ) ‘ 𝑑 ) = ∪ 𝑎 ∈ 𝑏 ( ( 𝑈 ‘ 𝑎 ) ‘ 𝑐 ) )
15 12 14 eqeq12d ⊢ ( 𝑑 = 𝑐 → ( ( ( 𝑈 ‘ 𝑏 ) ‘ suc 𝑑 ) = ∪ 𝑎 ∈ 𝑏 ( ( 𝑈 ‘ 𝑎 ) ‘ 𝑑 ) ↔ ( ( 𝑈 ‘ 𝑏 ) ‘ suc 𝑐 ) = ∪ 𝑎 ∈ 𝑏 ( ( 𝑈 ‘ 𝑎 ) ‘ 𝑐 ) ) )
16 suceq ⊢ ( 𝑑 = suc 𝑐 → suc 𝑑 = suc suc 𝑐 )
17 16 fveq2d ⊢ ( 𝑑 = suc 𝑐 → ( ( 𝑈 ‘ 𝑏 ) ‘ suc 𝑑 ) = ( ( 𝑈 ‘ 𝑏 ) ‘ suc suc 𝑐 ) )
18 fveq2 ⊢ ( 𝑑 = suc 𝑐 → ( ( 𝑈 ‘ 𝑎 ) ‘ 𝑑 ) = ( ( 𝑈 ‘ 𝑎 ) ‘ suc 𝑐 ) )
19 18 iuneq2d ⊢ ( 𝑑 = suc 𝑐 → ∪ 𝑎 ∈ 𝑏 ( ( 𝑈 ‘ 𝑎 ) ‘ 𝑑 ) = ∪ 𝑎 ∈ 𝑏 ( ( 𝑈 ‘ 𝑎 ) ‘ suc 𝑐 ) )
20 17 19 eqeq12d ⊢ ( 𝑑 = suc 𝑐 → ( ( ( 𝑈 ‘ 𝑏 ) ‘ suc 𝑑 ) = ∪ 𝑎 ∈ 𝑏 ( ( 𝑈 ‘ 𝑎 ) ‘ 𝑑 ) ↔ ( ( 𝑈 ‘ 𝑏 ) ‘ suc suc 𝑐 ) = ∪ 𝑎 ∈ 𝑏 ( ( 𝑈 ‘ 𝑎 ) ‘ suc 𝑐 ) ) )
21 suceq ⊢ ( 𝑑 = 𝐵 → suc 𝑑 = suc 𝐵 )
22 21 fveq2d ⊢ ( 𝑑 = 𝐵 → ( ( 𝑈 ‘ 𝑏 ) ‘ suc 𝑑 ) = ( ( 𝑈 ‘ 𝑏 ) ‘ suc 𝐵 ) )
23 fveq2 ⊢ ( 𝑑 = 𝐵 → ( ( 𝑈 ‘ 𝑎 ) ‘ 𝑑 ) = ( ( 𝑈 ‘ 𝑎 ) ‘ 𝐵 ) )
24 23 iuneq2d ⊢ ( 𝑑 = 𝐵 → ∪ 𝑎 ∈ 𝑏 ( ( 𝑈 ‘ 𝑎 ) ‘ 𝑑 ) = ∪ 𝑎 ∈ 𝑏 ( ( 𝑈 ‘ 𝑎 ) ‘ 𝐵 ) )
25 22 24 eqeq12d ⊢ ( 𝑑 = 𝐵 → ( ( ( 𝑈 ‘ 𝑏 ) ‘ suc 𝑑 ) = ∪ 𝑎 ∈ 𝑏 ( ( 𝑈 ‘ 𝑎 ) ‘ 𝑑 ) ↔ ( ( 𝑈 ‘ 𝑏 ) ‘ suc 𝐵 ) = ∪ 𝑎 ∈ 𝑏 ( ( 𝑈 ‘ 𝑎 ) ‘ 𝐵 ) ) )
26 uniiun ⊢ ∪ 𝑏 = ∪ 𝑎 ∈ 𝑏 𝑎
27 1 itunisuc ⊢ ( ( 𝑈 ‘ 𝑏 ) ‘ suc ∅ ) = ∪ ( ( 𝑈 ‘ 𝑏 ) ‘ ∅ )
28 1 ituni0 ⊢ ( 𝑏 ∈ V → ( ( 𝑈 ‘ 𝑏 ) ‘ ∅ ) = 𝑏 )
29 28 elv ⊢ ( ( 𝑈 ‘ 𝑏 ) ‘ ∅ ) = 𝑏
30 29 unieqi ⊢ ∪ ( ( 𝑈 ‘ 𝑏 ) ‘ ∅ ) = ∪ 𝑏
31 27 30 eqtri ⊢ ( ( 𝑈 ‘ 𝑏 ) ‘ suc ∅ ) = ∪ 𝑏
32 1 ituni0 ⊢ ( 𝑎 ∈ 𝑏 → ( ( 𝑈 ‘ 𝑎 ) ‘ ∅ ) = 𝑎 )
33 32 iuneq2i ⊢ ∪ 𝑎 ∈ 𝑏 ( ( 𝑈 ‘ 𝑎 ) ‘ ∅ ) = ∪ 𝑎 ∈ 𝑏 𝑎
34 26 31 33 3eqtr4i ⊢ ( ( 𝑈 ‘ 𝑏 ) ‘ suc ∅ ) = ∪ 𝑎 ∈ 𝑏 ( ( 𝑈 ‘ 𝑎 ) ‘ ∅ )
35 1 itunisuc ⊢ ( ( 𝑈 ‘ 𝑏 ) ‘ suc suc 𝑐 ) = ∪ ( ( 𝑈 ‘ 𝑏 ) ‘ suc 𝑐 )
36 unieq ⊢ ( ( ( 𝑈 ‘ 𝑏 ) ‘ suc 𝑐 ) = ∪ 𝑎 ∈ 𝑏 ( ( 𝑈 ‘ 𝑎 ) ‘ 𝑐 ) → ∪ ( ( 𝑈 ‘ 𝑏 ) ‘ suc 𝑐 ) = ∪ ∪ 𝑎 ∈ 𝑏 ( ( 𝑈 ‘ 𝑎 ) ‘ 𝑐 ) )
37 1 itunisuc ⊢ ( ( 𝑈 ‘ 𝑎 ) ‘ suc 𝑐 ) = ∪ ( ( 𝑈 ‘ 𝑎 ) ‘ 𝑐 )
38 37 a1i ⊢ ( 𝑎 ∈ 𝑏 → ( ( 𝑈 ‘ 𝑎 ) ‘ suc 𝑐 ) = ∪ ( ( 𝑈 ‘ 𝑎 ) ‘ 𝑐 ) )
39 38 iuneq2i ⊢ ∪ 𝑎 ∈ 𝑏 ( ( 𝑈 ‘ 𝑎 ) ‘ suc 𝑐 ) = ∪ 𝑎 ∈ 𝑏 ∪ ( ( 𝑈 ‘ 𝑎 ) ‘ 𝑐 )
40 iuncom4 ⊢ ∪ 𝑎 ∈ 𝑏 ∪ ( ( 𝑈 ‘ 𝑎 ) ‘ 𝑐 ) = ∪ ∪ 𝑎 ∈ 𝑏 ( ( 𝑈 ‘ 𝑎 ) ‘ 𝑐 )
41 39 40 eqtr2i ⊢ ∪ ∪ 𝑎 ∈ 𝑏 ( ( 𝑈 ‘ 𝑎 ) ‘ 𝑐 ) = ∪ 𝑎 ∈ 𝑏 ( ( 𝑈 ‘ 𝑎 ) ‘ suc 𝑐 )
42 36 41 eqtrdi ⊢ ( ( ( 𝑈 ‘ 𝑏 ) ‘ suc 𝑐 ) = ∪ 𝑎 ∈ 𝑏 ( ( 𝑈 ‘ 𝑎 ) ‘ 𝑐 ) → ∪ ( ( 𝑈 ‘ 𝑏 ) ‘ suc 𝑐 ) = ∪ 𝑎 ∈ 𝑏 ( ( 𝑈 ‘ 𝑎 ) ‘ suc 𝑐 ) )
43 35 42 eqtrid ⊢ ( ( ( 𝑈 ‘ 𝑏 ) ‘ suc 𝑐 ) = ∪ 𝑎 ∈ 𝑏 ( ( 𝑈 ‘ 𝑎 ) ‘ 𝑐 ) → ( ( 𝑈 ‘ 𝑏 ) ‘ suc suc 𝑐 ) = ∪ 𝑎 ∈ 𝑏 ( ( 𝑈 ‘ 𝑎 ) ‘ suc 𝑐 ) )
44 43 a1i ⊢ ( 𝑐 ∈ ω → ( ( ( 𝑈 ‘ 𝑏 ) ‘ suc 𝑐 ) = ∪ 𝑎 ∈ 𝑏 ( ( 𝑈 ‘ 𝑎 ) ‘ 𝑐 ) → ( ( 𝑈 ‘ 𝑏 ) ‘ suc suc 𝑐 ) = ∪ 𝑎 ∈ 𝑏 ( ( 𝑈 ‘ 𝑎 ) ‘ suc 𝑐 ) ) )
45 10 15 20 25 34 44 finds ⊢ ( 𝐵 ∈ ω → ( ( 𝑈 ‘ 𝑏 ) ‘ suc 𝐵 ) = ∪ 𝑎 ∈ 𝑏 ( ( 𝑈 ‘ 𝑎 ) ‘ 𝐵 ) )
46 iun0 ⊢ ∪ 𝑎 ∈ 𝑏 ∅ = ∅
47 46 eqcomi ⊢ ∅ = ∪ 𝑎 ∈ 𝑏 ∅
48 peano2b ⊢ ( 𝐵 ∈ ω ↔ suc 𝐵 ∈ ω )
49 vex ⊢ 𝑏 ∈ V
50 1 itunifn ⊢ ( 𝑏 ∈ V → ( 𝑈 ‘ 𝑏 ) Fn ω )
51 fndm ⊢ ( ( 𝑈 ‘ 𝑏 ) Fn ω → dom ( 𝑈 ‘ 𝑏 ) = ω )
52 49 50 51 mp2b ⊢ dom ( 𝑈 ‘ 𝑏 ) = ω
53 52 eleq2i ⊢ ( suc 𝐵 ∈ dom ( 𝑈 ‘ 𝑏 ) ↔ suc 𝐵 ∈ ω )
54 48 53 bitr4i ⊢ ( 𝐵 ∈ ω ↔ suc 𝐵 ∈ dom ( 𝑈 ‘ 𝑏 ) )
55 ndmfv ⊢ ( ¬ suc 𝐵 ∈ dom ( 𝑈 ‘ 𝑏 ) → ( ( 𝑈 ‘ 𝑏 ) ‘ suc 𝐵 ) = ∅ )
56 54 55 sylnbi ⊢ ( ¬ 𝐵 ∈ ω → ( ( 𝑈 ‘ 𝑏 ) ‘ suc 𝐵 ) = ∅ )
57 vex ⊢ 𝑎 ∈ V
58 1 itunifn ⊢ ( 𝑎 ∈ V → ( 𝑈 ‘ 𝑎 ) Fn ω )
59 fndm ⊢ ( ( 𝑈 ‘ 𝑎 ) Fn ω → dom ( 𝑈 ‘ 𝑎 ) = ω )
60 57 58 59 mp2b ⊢ dom ( 𝑈 ‘ 𝑎 ) = ω
61 60 eleq2i ⊢ ( 𝐵 ∈ dom ( 𝑈 ‘ 𝑎 ) ↔ 𝐵 ∈ ω )
62 ndmfv ⊢ ( ¬ 𝐵 ∈ dom ( 𝑈 ‘ 𝑎 ) → ( ( 𝑈 ‘ 𝑎 ) ‘ 𝐵 ) = ∅ )
63 61 62 sylnbir ⊢ ( ¬ 𝐵 ∈ ω → ( ( 𝑈 ‘ 𝑎 ) ‘ 𝐵 ) = ∅ )
64 63 iuneq2d ⊢ ( ¬ 𝐵 ∈ ω → ∪ 𝑎 ∈ 𝑏 ( ( 𝑈 ‘ 𝑎 ) ‘ 𝐵 ) = ∪ 𝑎 ∈ 𝑏 ∅ )
65 47 56 64 3eqtr4a ⊢ ( ¬ 𝐵 ∈ ω → ( ( 𝑈 ‘ 𝑏 ) ‘ suc 𝐵 ) = ∪ 𝑎 ∈ 𝑏 ( ( 𝑈 ‘ 𝑎 ) ‘ 𝐵 ) )
66 45 65 pm2.61i ⊢ ( ( 𝑈 ‘ 𝑏 ) ‘ suc 𝐵 ) = ∪ 𝑎 ∈ 𝑏 ( ( 𝑈 ‘ 𝑎 ) ‘ 𝐵 )
67 5 66 vtoclg ⊢ ( 𝐴 ∈ 𝑉 → ( ( 𝑈 ‘ 𝐴 ) ‘ suc 𝐵 ) = ∪ 𝑎 ∈ 𝐴 ( ( 𝑈 ‘ 𝑎 ) ‘ 𝐵 ) )