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 ⊢ 𝑈 = ( 𝑥 ∈ V ↦ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , 𝑥 ) ↾ ω ) )
Assertion itunitc1 ( ( 𝑈 ‘ 𝐴 ) ‘ 𝐵 ) ⊆ ( TC ‘ 𝐴 )

Proof

Step Hyp Ref Expression
1 ituni.u ⊢ 𝑈 = ( 𝑥 ∈ V ↦ ( rec ( ( 𝑦 ∈ V ↦ ∪ 𝑦 ) , 𝑥 ) ↾ ω ) )
2 fveq2 ⊢ ( 𝑎 = 𝐴 → ( 𝑈 ‘ 𝑎 ) = ( 𝑈 ‘ 𝐴 ) )
3 2 fveq1d ⊢ ( 𝑎 = 𝐴 → ( ( 𝑈 ‘ 𝑎 ) ‘ 𝐵 ) = ( ( 𝑈 ‘ 𝐴 ) ‘ 𝐵 ) )
4 fveq2 ⊢ ( 𝑎 = 𝐴 → ( TC ‘ 𝑎 ) = ( TC ‘ 𝐴 ) )
5 3 4 sseq12d ⊢ ( 𝑎 = 𝐴 → ( ( ( 𝑈 ‘ 𝑎 ) ‘ 𝐵 ) ⊆ ( TC ‘ 𝑎 ) ↔ ( ( 𝑈 ‘ 𝐴 ) ‘ 𝐵 ) ⊆ ( TC ‘ 𝐴 ) ) )
6 fveq2 ⊢ ( 𝑏 = ∅ → ( ( 𝑈 ‘ 𝑎 ) ‘ 𝑏 ) = ( ( 𝑈 ‘ 𝑎 ) ‘ ∅ ) )
7 6 sseq1d ⊢ ( 𝑏 = ∅ → ( ( ( 𝑈 ‘ 𝑎 ) ‘ 𝑏 ) ⊆ ( TC ‘ 𝑎 ) ↔ ( ( 𝑈 ‘ 𝑎 ) ‘ ∅ ) ⊆ ( TC ‘ 𝑎 ) ) )
8 fveq2 ⊢ ( 𝑏 = 𝑐 → ( ( 𝑈 ‘ 𝑎 ) ‘ 𝑏 ) = ( ( 𝑈 ‘ 𝑎 ) ‘ 𝑐 ) )
9 8 sseq1d ⊢ ( 𝑏 = 𝑐 → ( ( ( 𝑈 ‘ 𝑎 ) ‘ 𝑏 ) ⊆ ( TC ‘ 𝑎 ) ↔ ( ( 𝑈 ‘ 𝑎 ) ‘ 𝑐 ) ⊆ ( TC ‘ 𝑎 ) ) )
10 fveq2 ⊢ ( 𝑏 = suc 𝑐 → ( ( 𝑈 ‘ 𝑎 ) ‘ 𝑏 ) = ( ( 𝑈 ‘ 𝑎 ) ‘ suc 𝑐 ) )
11 10 sseq1d ⊢ ( 𝑏 = suc 𝑐 → ( ( ( 𝑈 ‘ 𝑎 ) ‘ 𝑏 ) ⊆ ( TC ‘ 𝑎 ) ↔ ( ( 𝑈 ‘ 𝑎 ) ‘ suc 𝑐 ) ⊆ ( TC ‘ 𝑎 ) ) )
12 fveq2 ⊢ ( 𝑏 = 𝐵 → ( ( 𝑈 ‘ 𝑎 ) ‘ 𝑏 ) = ( ( 𝑈 ‘ 𝑎 ) ‘ 𝐵 ) )
13 12 sseq1d ⊢ ( 𝑏 = 𝐵 → ( ( ( 𝑈 ‘ 𝑎 ) ‘ 𝑏 ) ⊆ ( TC ‘ 𝑎 ) ↔ ( ( 𝑈 ‘ 𝑎 ) ‘ 𝐵 ) ⊆ ( TC ‘ 𝑎 ) ) )
14 1 ituni0 ⊢ ( 𝑎 ∈ V → ( ( 𝑈 ‘ 𝑎 ) ‘ ∅ ) = 𝑎 )
15 tcid ⊢ ( 𝑎 ∈ V → 𝑎 ⊆ ( TC ‘ 𝑎 ) )
16 14 15 eqsstrd ⊢ ( 𝑎 ∈ V → ( ( 𝑈 ‘ 𝑎 ) ‘ ∅ ) ⊆ ( TC ‘ 𝑎 ) )
17 16 elv ⊢ ( ( 𝑈 ‘ 𝑎 ) ‘ ∅ ) ⊆ ( TC ‘ 𝑎 )
18 1 itunisuc ⊢ ( ( 𝑈 ‘ 𝑎 ) ‘ suc 𝑐 ) = ∪ ( ( 𝑈 ‘ 𝑎 ) ‘ 𝑐 )
19 tctr ⊢ Tr ( TC ‘ 𝑎 )
20 pwtr ⊢ ( Tr ( TC ‘ 𝑎 ) ↔ Tr 𝒫 ( TC ‘ 𝑎 ) )
21 19 20 mpbi ⊢ Tr 𝒫 ( TC ‘ 𝑎 )
22 trss ⊢ ( Tr 𝒫 ( TC ‘ 𝑎 ) → ( ( ( 𝑈 ‘ 𝑎 ) ‘ 𝑐 ) ∈ 𝒫 ( TC ‘ 𝑎 ) → ( ( 𝑈 ‘ 𝑎 ) ‘ 𝑐 ) ⊆ 𝒫 ( TC ‘ 𝑎 ) ) )
23 21 22 ax-mp ⊢ ( ( ( 𝑈 ‘ 𝑎 ) ‘ 𝑐 ) ∈ 𝒫 ( TC ‘ 𝑎 ) → ( ( 𝑈 ‘ 𝑎 ) ‘ 𝑐 ) ⊆ 𝒫 ( TC ‘ 𝑎 ) )
24 fvex ⊢ ( ( 𝑈 ‘ 𝑎 ) ‘ 𝑐 ) ∈ V
25 24 elpw ⊢ ( ( ( 𝑈 ‘ 𝑎 ) ‘ 𝑐 ) ∈ 𝒫 ( TC ‘ 𝑎 ) ↔ ( ( 𝑈 ‘ 𝑎 ) ‘ 𝑐 ) ⊆ ( TC ‘ 𝑎 ) )
26 sspwuni ⊢ ( ( ( 𝑈 ‘ 𝑎 ) ‘ 𝑐 ) ⊆ 𝒫 ( TC ‘ 𝑎 ) ↔ ∪ ( ( 𝑈 ‘ 𝑎 ) ‘ 𝑐 ) ⊆ ( TC ‘ 𝑎 ) )
27 23 25 26 3imtr3i ⊢ ( ( ( 𝑈 ‘ 𝑎 ) ‘ 𝑐 ) ⊆ ( TC ‘ 𝑎 ) → ∪ ( ( 𝑈 ‘ 𝑎 ) ‘ 𝑐 ) ⊆ ( TC ‘ 𝑎 ) )
28 18 27 eqsstrid ⊢ ( ( ( 𝑈 ‘ 𝑎 ) ‘ 𝑐 ) ⊆ ( TC ‘ 𝑎 ) → ( ( 𝑈 ‘ 𝑎 ) ‘ suc 𝑐 ) ⊆ ( TC ‘ 𝑎 ) )
29 28 a1i ⊢ ( 𝑐 ∈ ω → ( ( ( 𝑈 ‘ 𝑎 ) ‘ 𝑐 ) ⊆ ( TC ‘ 𝑎 ) → ( ( 𝑈 ‘ 𝑎 ) ‘ suc 𝑐 ) ⊆ ( TC ‘ 𝑎 ) ) )
30 7 9 11 13 17 29 finds ⊢ ( 𝐵 ∈ ω → ( ( 𝑈 ‘ 𝑎 ) ‘ 𝐵 ) ⊆ ( TC ‘ 𝑎 ) )
31 vex ⊢ 𝑎 ∈ V
32 1 itunifn ⊢ ( 𝑎 ∈ V → ( 𝑈 ‘ 𝑎 ) Fn ω )
33 fndm ⊢ ( ( 𝑈 ‘ 𝑎 ) Fn ω → dom ( 𝑈 ‘ 𝑎 ) = ω )
34 31 32 33 mp2b ⊢ dom ( 𝑈 ‘ 𝑎 ) = ω
35 34 eleq2i ⊢ ( 𝐵 ∈ dom ( 𝑈 ‘ 𝑎 ) ↔ 𝐵 ∈ ω )
36 ndmfv ⊢ ( ¬ 𝐵 ∈ dom ( 𝑈 ‘ 𝑎 ) → ( ( 𝑈 ‘ 𝑎 ) ‘ 𝐵 ) = ∅ )
37 35 36 sylnbir ⊢ ( ¬ 𝐵 ∈ ω → ( ( 𝑈 ‘ 𝑎 ) ‘ 𝐵 ) = ∅ )
38 0ss ⊢ ∅ ⊆ ( TC ‘ 𝑎 )
39 37 38 eqsstrdi ⊢ ( ¬ 𝐵 ∈ ω → ( ( 𝑈 ‘ 𝑎 ) ‘ 𝐵 ) ⊆ ( TC ‘ 𝑎 ) )
40 30 39 pm2.61i ⊢ ( ( 𝑈 ‘ 𝑎 ) ‘ 𝐵 ) ⊆ ( TC ‘ 𝑎 )
41 5 40 vtoclg ⊢ ( 𝐴 ∈ V → ( ( 𝑈 ‘ 𝐴 ) ‘ 𝐵 ) ⊆ ( TC ‘ 𝐴 ) )
42 fv2prc ⊢ ( ¬ 𝐴 ∈ V → ( ( 𝑈 ‘ 𝐴 ) ‘ 𝐵 ) = ∅ )
43 0ss ⊢ ∅ ⊆ ( TC ‘ 𝐴 )
44 42 43 eqsstrdi ⊢ ( ¬ 𝐴 ∈ V → ( ( 𝑈 ‘ 𝐴 ) ‘ 𝐵 ) ⊆ ( TC ‘ 𝐴 ) )
45 41 44 pm2.61i ⊢ ( ( 𝑈 ‘ 𝐴 ) ‘ 𝐵 ) ⊆ ( TC ‘ 𝐴 )