Metamath Proof Explorer

Theorem itunitc1

Description: Each union iterate is a member of the transitive closure. (Contributed by Stefan O'Rear, 11-Feb-2015)

Ref Expression
Hypothesis ituni.u ⊢U=x∈V⟼rec⁡y∈V⟼⋃yx↾ω
Assertion itunitc1 ⊢U⁡A⁡B⊆TC⁡A

Proof

Step Hyp Ref Expression
1 ituni.u ⊢U=x∈V⟼rec⁡y∈V⟼⋃yx↾ω
2 fveq2 ⊢a=A→U⁡a=U⁡A
3 2 fveq1d ⊢a=A→U⁡a⁡B=U⁡A⁡B
4 fveq2 ⊢a=A→TC⁡a=TC⁡A
5 3 4 sseq12d ⊢a=A→U⁡a⁡B⊆TC⁡a↔U⁡A⁡B⊆TC⁡A
6 fveq2 ⊢b=∅→U⁡a⁡b=U⁡a⁡∅
7 6 sseq1d ⊢b=∅→U⁡a⁡b⊆TC⁡a↔U⁡a⁡∅⊆TC⁡a
8 fveq2 ⊢b=c→U⁡a⁡b=U⁡a⁡c
9 8 sseq1d ⊢b=c→U⁡a⁡b⊆TC⁡a↔U⁡a⁡c⊆TC⁡a
10 fveq2 ⊢b=suc⁡c→U⁡a⁡b=U⁡a⁡suc⁡c
11 10 sseq1d ⊢b=suc⁡c→U⁡a⁡b⊆TC⁡a↔U⁡a⁡suc⁡c⊆TC⁡a
12 fveq2 ⊢b=B→U⁡a⁡b=U⁡a⁡B
13 12 sseq1d ⊢b=B→U⁡a⁡b⊆TC⁡a↔U⁡a⁡B⊆TC⁡a
14 1 ituni0 ⊢a∈V→U⁡a⁡∅=a
15 tcid ⊢a∈V→a⊆TC⁡a
16 14 15 eqsstrd ⊢a∈V→U⁡a⁡∅⊆TC⁡a
17 16 elv ⊢U⁡a⁡∅⊆TC⁡a
18 1 itunisuc ⊢U⁡a⁡suc⁡c=⋃U⁡a⁡c
19 tctr ⊢Tr⁡TC⁡a
20 pwtr ⊢Tr⁡TC⁡a↔Tr⁡𝒫TC⁡a
21 19 20 mpbi ⊢Tr⁡𝒫TC⁡a
22 trss ⊢Tr⁡𝒫TC⁡a→U⁡a⁡c∈𝒫TC⁡a→U⁡a⁡c⊆𝒫TC⁡a
23 21 22 ax-mp ⊢U⁡a⁡c∈𝒫TC⁡a→U⁡a⁡c⊆𝒫TC⁡a
24 fvex ⊢U⁡a⁡c∈V
25 24 elpw ⊢U⁡a⁡c∈𝒫TC⁡a↔U⁡a⁡c⊆TC⁡a
26 sspwuni ⊢U⁡a⁡c⊆𝒫TC⁡a↔⋃U⁡a⁡c⊆TC⁡a
27 23 25 26 3imtr3i ⊢U⁡a⁡c⊆TC⁡a→⋃U⁡a⁡c⊆TC⁡a
28 18 27 eqsstrid ⊢U⁡a⁡c⊆TC⁡a→U⁡a⁡suc⁡c⊆TC⁡a
29 28 a1i ⊢c∈ω→U⁡a⁡c⊆TC⁡a→U⁡a⁡suc⁡c⊆TC⁡a
30 7 9 11 13 17 29 finds ⊢B∈ω→U⁡a⁡B⊆TC⁡a
31 vex ⊢a∈V
32 1 itunifn ⊢a∈V→U⁡aFnω
33 fndm ⊢U⁡aFnω→dom⁡U⁡a=ω
34 31 32 33 mp2b ⊢dom⁡U⁡a=ω
35 34 eleq2i ⊢B∈dom⁡U⁡a↔B∈ω
36 ndmfv ⊢¬B∈dom⁡U⁡a→U⁡a⁡B=∅
37 35 36 sylnbir ⊢¬B∈ω→U⁡a⁡B=∅
38 0ss ⊢∅⊆TC⁡a
39 37 38 eqsstrdi ⊢¬B∈ω→U⁡a⁡B⊆TC⁡a
40 30 39 pm2.61i ⊢U⁡a⁡B⊆TC⁡a
41 5 40 vtoclg ⊢A∈V→U⁡A⁡B⊆TC⁡A
42 fv2prc ⊢¬A∈V→U⁡A⁡B=∅
43 0ss ⊢∅⊆TC⁡A
44 42 43 eqsstrdi ⊢¬A∈V→U⁡A⁡B⊆TC⁡A
45 41 44 pm2.61i ⊢U⁡A⁡B⊆TC⁡A