Metamath Proof Explorer

Theorem trcl

Description: For any set A , show the properties of its transitive closure C . Similar to Theorem 9.1 of TakeutiZaring p. 73 except that we show an explicit expression for the transitive closure rather than just its existence. See tz9.1 for an abbreviated version showing existence. (Contributed by NM, 14-Sep-2003) (Revised by Mario Carneiro, 11-Sep-2015)

Ref Expression
Hypotheses trcl.1 ⊢ 𝐴 ∈ V
trcl.2 ⊢ 𝐹 = ( rec ( ( 𝑧 ∈ V ↦ ( 𝑧 ∪ ∪ 𝑧 ) ) , 𝐴 ) ↾ ω )
trcl.3 ⊢ 𝐶 = ∪ 𝑦 ∈ ω ( 𝐹 ‘ 𝑦 )
Assertion trcl ( 𝐴 ⊆ 𝐶 ∧ Tr 𝐶 ∧ ∀ 𝑥 ( ( 𝐴 ⊆ 𝑥 ∧ Tr 𝑥 ) → 𝐶 ⊆ 𝑥 ) )

Proof

Step Hyp Ref Expression
1 trcl.1 ⊢ 𝐴 ∈ V
2 trcl.2 ⊢ 𝐹 = ( rec ( ( 𝑧 ∈ V ↦ ( 𝑧 ∪ ∪ 𝑧 ) ) , 𝐴 ) ↾ ω )
3 trcl.3 ⊢ 𝐶 = ∪ 𝑦 ∈ ω ( 𝐹 ‘ 𝑦 )
4 peano1 ⊢ ∅ ∈ ω
5 2 fveq1i ⊢ ( 𝐹 ‘ ∅ ) = ( ( rec ( ( 𝑧 ∈ V ↦ ( 𝑧 ∪ ∪ 𝑧 ) ) , 𝐴 ) ↾ ω ) ‘ ∅ )
6 fr0g ⊢ ( 𝐴 ∈ V → ( ( rec ( ( 𝑧 ∈ V ↦ ( 𝑧 ∪ ∪ 𝑧 ) ) , 𝐴 ) ↾ ω ) ‘ ∅ ) = 𝐴 )
7 1 6 ax-mp ⊢ ( ( rec ( ( 𝑧 ∈ V ↦ ( 𝑧 ∪ ∪ 𝑧 ) ) , 𝐴 ) ↾ ω ) ‘ ∅ ) = 𝐴
8 5 7 eqtr2i ⊢ 𝐴 = ( 𝐹 ‘ ∅ )
9 8 eqimssi ⊢ 𝐴 ⊆ ( 𝐹 ‘ ∅ )
10 fveq2 ⊢ ( 𝑦 = ∅ → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ ∅ ) )
11 10 sseq2d ⊢ ( 𝑦 = ∅ → ( 𝐴 ⊆ ( 𝐹 ‘ 𝑦 ) ↔ 𝐴 ⊆ ( 𝐹 ‘ ∅ ) ) )
12 11 rspcev ⊢ ( ( ∅ ∈ ω ∧ 𝐴 ⊆ ( 𝐹 ‘ ∅ ) ) → ∃ 𝑦 ∈ ω 𝐴 ⊆ ( 𝐹 ‘ 𝑦 ) )
13 4 9 12 mp2an ⊢ ∃ 𝑦 ∈ ω 𝐴 ⊆ ( 𝐹 ‘ 𝑦 )
14 ssiun ⊢ ( ∃ 𝑦 ∈ ω 𝐴 ⊆ ( 𝐹 ‘ 𝑦 ) → 𝐴 ⊆ ∪ 𝑦 ∈ ω ( 𝐹 ‘ 𝑦 ) )
15 13 14 ax-mp ⊢ 𝐴 ⊆ ∪ 𝑦 ∈ ω ( 𝐹 ‘ 𝑦 )
16 15 3 sseqtrri ⊢ 𝐴 ⊆ 𝐶
17 dftr2 ⊢ ( Tr ∪ 𝑦 ∈ ω ( 𝐹 ‘ 𝑦 ) ↔ ∀ 𝑣 ∀ 𝑢 ( ( 𝑣 ∈ 𝑢 ∧ 𝑢 ∈ ∪ 𝑦 ∈ ω ( 𝐹 ‘ 𝑦 ) ) → 𝑣 ∈ ∪ 𝑦 ∈ ω ( 𝐹 ‘ 𝑦 ) ) )
18 eliun ⊢ ( 𝑢 ∈ ∪ 𝑦 ∈ ω ( 𝐹 ‘ 𝑦 ) ↔ ∃ 𝑦 ∈ ω 𝑢 ∈ ( 𝐹 ‘ 𝑦 ) )
19 18 anbi2i ⊢ ( ( 𝑣 ∈ 𝑢 ∧ 𝑢 ∈ ∪ 𝑦 ∈ ω ( 𝐹 ‘ 𝑦 ) ) ↔ ( 𝑣 ∈ 𝑢 ∧ ∃ 𝑦 ∈ ω 𝑢 ∈ ( 𝐹 ‘ 𝑦 ) ) )
20 r19.42v ⊢ ( ∃ 𝑦 ∈ ω ( 𝑣 ∈ 𝑢 ∧ 𝑢 ∈ ( 𝐹 ‘ 𝑦 ) ) ↔ ( 𝑣 ∈ 𝑢 ∧ ∃ 𝑦 ∈ ω 𝑢 ∈ ( 𝐹 ‘ 𝑦 ) ) )
21 19 20 bitr4i ⊢ ( ( 𝑣 ∈ 𝑢 ∧ 𝑢 ∈ ∪ 𝑦 ∈ ω ( 𝐹 ‘ 𝑦 ) ) ↔ ∃ 𝑦 ∈ ω ( 𝑣 ∈ 𝑢 ∧ 𝑢 ∈ ( 𝐹 ‘ 𝑦 ) ) )
22 elunii ⊢ ( ( 𝑣 ∈ 𝑢 ∧ 𝑢 ∈ ( 𝐹 ‘ 𝑦 ) ) → 𝑣 ∈ ∪ ( 𝐹 ‘ 𝑦 ) )
23 ssun2 ⊢ ∪ ( 𝐹 ‘ 𝑦 ) ⊆ ( ( 𝐹 ‘ 𝑦 ) ∪ ∪ ( 𝐹 ‘ 𝑦 ) )
24 fvex ⊢ ( 𝐹 ‘ 𝑦 ) ∈ V
25 24 uniex ⊢ ∪ ( 𝐹 ‘ 𝑦 ) ∈ V
26 24 25 unex ⊢ ( ( 𝐹 ‘ 𝑦 ) ∪ ∪ ( 𝐹 ‘ 𝑦 ) ) ∈ V
27 id ⊢ ( 𝑥 = 𝑧 → 𝑥 = 𝑧 )
28 unieq ⊢ ( 𝑥 = 𝑧 → ∪ 𝑥 = ∪ 𝑧 )
29 27 28 uneq12d ⊢ ( 𝑥 = 𝑧 → ( 𝑥 ∪ ∪ 𝑥 ) = ( 𝑧 ∪ ∪ 𝑧 ) )
30 id ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑦 ) → 𝑥 = ( 𝐹 ‘ 𝑦 ) )
31 unieq ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑦 ) → ∪ 𝑥 = ∪ ( 𝐹 ‘ 𝑦 ) )
32 30 31 uneq12d ⊢ ( 𝑥 = ( 𝐹 ‘ 𝑦 ) → ( 𝑥 ∪ ∪ 𝑥 ) = ( ( 𝐹 ‘ 𝑦 ) ∪ ∪ ( 𝐹 ‘ 𝑦 ) ) )
33 2 29 32 frsucmpt2 ⊢ ( ( 𝑦 ∈ ω ∧ ( ( 𝐹 ‘ 𝑦 ) ∪ ∪ ( 𝐹 ‘ 𝑦 ) ) ∈ V ) → ( 𝐹 ‘ suc 𝑦 ) = ( ( 𝐹 ‘ 𝑦 ) ∪ ∪ ( 𝐹 ‘ 𝑦 ) ) )
34 26 33 mpan2 ⊢ ( 𝑦 ∈ ω → ( 𝐹 ‘ suc 𝑦 ) = ( ( 𝐹 ‘ 𝑦 ) ∪ ∪ ( 𝐹 ‘ 𝑦 ) ) )
35 23 34 sseqtrrid ⊢ ( 𝑦 ∈ ω → ∪ ( 𝐹 ‘ 𝑦 ) ⊆ ( 𝐹 ‘ suc 𝑦 ) )
36 35 sseld ⊢ ( 𝑦 ∈ ω → ( 𝑣 ∈ ∪ ( 𝐹 ‘ 𝑦 ) → 𝑣 ∈ ( 𝐹 ‘ suc 𝑦 ) ) )
37 22 36 syl5 ⊢ ( 𝑦 ∈ ω → ( ( 𝑣 ∈ 𝑢 ∧ 𝑢 ∈ ( 𝐹 ‘ 𝑦 ) ) → 𝑣 ∈ ( 𝐹 ‘ suc 𝑦 ) ) )
38 37 reximia ⊢ ( ∃ 𝑦 ∈ ω ( 𝑣 ∈ 𝑢 ∧ 𝑢 ∈ ( 𝐹 ‘ 𝑦 ) ) → ∃ 𝑦 ∈ ω 𝑣 ∈ ( 𝐹 ‘ suc 𝑦 ) )
39 21 38 sylbi ⊢ ( ( 𝑣 ∈ 𝑢 ∧ 𝑢 ∈ ∪ 𝑦 ∈ ω ( 𝐹 ‘ 𝑦 ) ) → ∃ 𝑦 ∈ ω 𝑣 ∈ ( 𝐹 ‘ suc 𝑦 ) )
40 peano2 ⊢ ( 𝑦 ∈ ω → suc 𝑦 ∈ ω )
41 fveq2 ⊢ ( 𝑢 = suc 𝑦 → ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ suc 𝑦 ) )
42 41 eleq2d ⊢ ( 𝑢 = suc 𝑦 → ( 𝑣 ∈ ( 𝐹 ‘ 𝑢 ) ↔ 𝑣 ∈ ( 𝐹 ‘ suc 𝑦 ) ) )
43 42 rspcev ⊢ ( ( suc 𝑦 ∈ ω ∧ 𝑣 ∈ ( 𝐹 ‘ suc 𝑦 ) ) → ∃ 𝑢 ∈ ω 𝑣 ∈ ( 𝐹 ‘ 𝑢 ) )
44 43 ex ⊢ ( suc 𝑦 ∈ ω → ( 𝑣 ∈ ( 𝐹 ‘ suc 𝑦 ) → ∃ 𝑢 ∈ ω 𝑣 ∈ ( 𝐹 ‘ 𝑢 ) ) )
45 40 44 syl ⊢ ( 𝑦 ∈ ω → ( 𝑣 ∈ ( 𝐹 ‘ suc 𝑦 ) → ∃ 𝑢 ∈ ω 𝑣 ∈ ( 𝐹 ‘ 𝑢 ) ) )
46 45 rexlimiv ⊢ ( ∃ 𝑦 ∈ ω 𝑣 ∈ ( 𝐹 ‘ suc 𝑦 ) → ∃ 𝑢 ∈ ω 𝑣 ∈ ( 𝐹 ‘ 𝑢 ) )
47 fveq2 ⊢ ( 𝑦 = 𝑢 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑢 ) )
48 47 eleq2d ⊢ ( 𝑦 = 𝑢 → ( 𝑣 ∈ ( 𝐹 ‘ 𝑦 ) ↔ 𝑣 ∈ ( 𝐹 ‘ 𝑢 ) ) )
49 48 cbvrexvw ⊢ ( ∃ 𝑦 ∈ ω 𝑣 ∈ ( 𝐹 ‘ 𝑦 ) ↔ ∃ 𝑢 ∈ ω 𝑣 ∈ ( 𝐹 ‘ 𝑢 ) )
50 46 49 sylibr ⊢ ( ∃ 𝑦 ∈ ω 𝑣 ∈ ( 𝐹 ‘ suc 𝑦 ) → ∃ 𝑦 ∈ ω 𝑣 ∈ ( 𝐹 ‘ 𝑦 ) )
51 eliun ⊢ ( 𝑣 ∈ ∪ 𝑦 ∈ ω ( 𝐹 ‘ 𝑦 ) ↔ ∃ 𝑦 ∈ ω 𝑣 ∈ ( 𝐹 ‘ 𝑦 ) )
52 50 51 sylibr ⊢ ( ∃ 𝑦 ∈ ω 𝑣 ∈ ( 𝐹 ‘ suc 𝑦 ) → 𝑣 ∈ ∪ 𝑦 ∈ ω ( 𝐹 ‘ 𝑦 ) )
53 39 52 syl ⊢ ( ( 𝑣 ∈ 𝑢 ∧ 𝑢 ∈ ∪ 𝑦 ∈ ω ( 𝐹 ‘ 𝑦 ) ) → 𝑣 ∈ ∪ 𝑦 ∈ ω ( 𝐹 ‘ 𝑦 ) )
54 53 ax-gen ⊢ ∀ 𝑢 ( ( 𝑣 ∈ 𝑢 ∧ 𝑢 ∈ ∪ 𝑦 ∈ ω ( 𝐹 ‘ 𝑦 ) ) → 𝑣 ∈ ∪ 𝑦 ∈ ω ( 𝐹 ‘ 𝑦 ) )
55 17 54 mpgbir ⊢ Tr ∪ 𝑦 ∈ ω ( 𝐹 ‘ 𝑦 )
56 treq ⊢ ( 𝐶 = ∪ 𝑦 ∈ ω ( 𝐹 ‘ 𝑦 ) → ( Tr 𝐶 ↔ Tr ∪ 𝑦 ∈ ω ( 𝐹 ‘ 𝑦 ) ) )
57 3 56 ax-mp ⊢ ( Tr 𝐶 ↔ Tr ∪ 𝑦 ∈ ω ( 𝐹 ‘ 𝑦 ) )
58 55 57 mpbir ⊢ Tr 𝐶
59 fveq2 ⊢ ( 𝑣 = ∅ → ( 𝐹 ‘ 𝑣 ) = ( 𝐹 ‘ ∅ ) )
60 59 sseq1d ⊢ ( 𝑣 = ∅ → ( ( 𝐹 ‘ 𝑣 ) ⊆ 𝑥 ↔ ( 𝐹 ‘ ∅ ) ⊆ 𝑥 ) )
61 fveq2 ⊢ ( 𝑣 = 𝑦 → ( 𝐹 ‘ 𝑣 ) = ( 𝐹 ‘ 𝑦 ) )
62 61 sseq1d ⊢ ( 𝑣 = 𝑦 → ( ( 𝐹 ‘ 𝑣 ) ⊆ 𝑥 ↔ ( 𝐹 ‘ 𝑦 ) ⊆ 𝑥 ) )
63 fveq2 ⊢ ( 𝑣 = suc 𝑦 → ( 𝐹 ‘ 𝑣 ) = ( 𝐹 ‘ suc 𝑦 ) )
64 63 sseq1d ⊢ ( 𝑣 = suc 𝑦 → ( ( 𝐹 ‘ 𝑣 ) ⊆ 𝑥 ↔ ( 𝐹 ‘ suc 𝑦 ) ⊆ 𝑥 ) )
65 5 7 eqtri ⊢ ( 𝐹 ‘ ∅ ) = 𝐴
66 65 sseq1i ⊢ ( ( 𝐹 ‘ ∅ ) ⊆ 𝑥 ↔ 𝐴 ⊆ 𝑥 )
67 66 biranri ⊢ ( ( 𝐴 ⊆ 𝑥 ∧ Tr 𝑥 ) → ( 𝐹 ‘ ∅ ) ⊆ 𝑥 )
68 uniss ⊢ ( ( 𝐹 ‘ 𝑦 ) ⊆ 𝑥 → ∪ ( 𝐹 ‘ 𝑦 ) ⊆ ∪ 𝑥 )
69 df-tr ⊢ ( Tr 𝑥 ↔ ∪ 𝑥 ⊆ 𝑥 )
70 sstr2 ⊢ ( ∪ ( 𝐹 ‘ 𝑦 ) ⊆ ∪ 𝑥 → ( ∪ 𝑥 ⊆ 𝑥 → ∪ ( 𝐹 ‘ 𝑦 ) ⊆ 𝑥 ) )
71 69 70 biimtrid ⊢ ( ∪ ( 𝐹 ‘ 𝑦 ) ⊆ ∪ 𝑥 → ( Tr 𝑥 → ∪ ( 𝐹 ‘ 𝑦 ) ⊆ 𝑥 ) )
72 68 71 syl ⊢ ( ( 𝐹 ‘ 𝑦 ) ⊆ 𝑥 → ( Tr 𝑥 → ∪ ( 𝐹 ‘ 𝑦 ) ⊆ 𝑥 ) )
73 72 anc2li ⊢ ( ( 𝐹 ‘ 𝑦 ) ⊆ 𝑥 → ( Tr 𝑥 → ( ( 𝐹 ‘ 𝑦 ) ⊆ 𝑥 ∧ ∪ ( 𝐹 ‘ 𝑦 ) ⊆ 𝑥 ) ) )
74 unss ⊢ ( ( ( 𝐹 ‘ 𝑦 ) ⊆ 𝑥 ∧ ∪ ( 𝐹 ‘ 𝑦 ) ⊆ 𝑥 ) ↔ ( ( 𝐹 ‘ 𝑦 ) ∪ ∪ ( 𝐹 ‘ 𝑦 ) ) ⊆ 𝑥 )
75 73 74 imbitrdi ⊢ ( ( 𝐹 ‘ 𝑦 ) ⊆ 𝑥 → ( Tr 𝑥 → ( ( 𝐹 ‘ 𝑦 ) ∪ ∪ ( 𝐹 ‘ 𝑦 ) ) ⊆ 𝑥 ) )
76 34 sseq1d ⊢ ( 𝑦 ∈ ω → ( ( 𝐹 ‘ suc 𝑦 ) ⊆ 𝑥 ↔ ( ( 𝐹 ‘ 𝑦 ) ∪ ∪ ( 𝐹 ‘ 𝑦 ) ) ⊆ 𝑥 ) )
77 76 biimprd ⊢ ( 𝑦 ∈ ω → ( ( ( 𝐹 ‘ 𝑦 ) ∪ ∪ ( 𝐹 ‘ 𝑦 ) ) ⊆ 𝑥 → ( 𝐹 ‘ suc 𝑦 ) ⊆ 𝑥 ) )
78 75 77 syl9r ⊢ ( 𝑦 ∈ ω → ( ( 𝐹 ‘ 𝑦 ) ⊆ 𝑥 → ( Tr 𝑥 → ( 𝐹 ‘ suc 𝑦 ) ⊆ 𝑥 ) ) )
79 78 com23 ⊢ ( 𝑦 ∈ ω → ( Tr 𝑥 → ( ( 𝐹 ‘ 𝑦 ) ⊆ 𝑥 → ( 𝐹 ‘ suc 𝑦 ) ⊆ 𝑥 ) ) )
80 79 adantld ⊢ ( 𝑦 ∈ ω → ( ( 𝐴 ⊆ 𝑥 ∧ Tr 𝑥 ) → ( ( 𝐹 ‘ 𝑦 ) ⊆ 𝑥 → ( 𝐹 ‘ suc 𝑦 ) ⊆ 𝑥 ) ) )
81 60 62 64 67 80 finds2 ⊢ ( 𝑣 ∈ ω → ( ( 𝐴 ⊆ 𝑥 ∧ Tr 𝑥 ) → ( 𝐹 ‘ 𝑣 ) ⊆ 𝑥 ) )
82 81 com12 ⊢ ( ( 𝐴 ⊆ 𝑥 ∧ Tr 𝑥 ) → ( 𝑣 ∈ ω → ( 𝐹 ‘ 𝑣 ) ⊆ 𝑥 ) )
83 82 ralrimiv ⊢ ( ( 𝐴 ⊆ 𝑥 ∧ Tr 𝑥 ) → ∀ 𝑣 ∈ ω ( 𝐹 ‘ 𝑣 ) ⊆ 𝑥 )
84 fveq2 ⊢ ( 𝑦 = 𝑣 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑣 ) )
85 84 cbviunv ⊢ ∪ 𝑦 ∈ ω ( 𝐹 ‘ 𝑦 ) = ∪ 𝑣 ∈ ω ( 𝐹 ‘ 𝑣 )
86 3 85 eqtri ⊢ 𝐶 = ∪ 𝑣 ∈ ω ( 𝐹 ‘ 𝑣 )
87 86 sseq1i ⊢ ( 𝐶 ⊆ 𝑥 ↔ ∪ 𝑣 ∈ ω ( 𝐹 ‘ 𝑣 ) ⊆ 𝑥 )
88 iunss ⊢ ( ∪ 𝑣 ∈ ω ( 𝐹 ‘ 𝑣 ) ⊆ 𝑥 ↔ ∀ 𝑣 ∈ ω ( 𝐹 ‘ 𝑣 ) ⊆ 𝑥 )
89 87 88 bitri ⊢ ( 𝐶 ⊆ 𝑥 ↔ ∀ 𝑣 ∈ ω ( 𝐹 ‘ 𝑣 ) ⊆ 𝑥 )
90 83 89 sylibr ⊢ ( ( 𝐴 ⊆ 𝑥 ∧ Tr 𝑥 ) → 𝐶 ⊆ 𝑥 )
91 90 ax-gen ⊢ ∀ 𝑥 ( ( 𝐴 ⊆ 𝑥 ∧ Tr 𝑥 ) → 𝐶 ⊆ 𝑥 )
92 16 58 91 3pm3.2i ⊢ ( 𝐴 ⊆ 𝐶 ∧ Tr 𝐶 ∧ ∀ 𝑥 ( ( 𝐴 ⊆ 𝑥 ∧ Tr 𝑥 ) → 𝐶 ⊆ 𝑥 ) )