Metamath Proof Explorer

Theorem ttcid

Description: The transitive closure contains its argument as a subclass. (Contributed by Matthew House, 6-Apr-2026)

Ref Expression
Assertion ttcid Could not format assertion : No typesetting found for |- A C_ TC+ A with typecode |-

Proof

Step Hyp Ref Expression
1 vsnid ⊢ z ∈ z
2 vsnex ⊢ z ∈ V
3 2 rdg0 ⊢ rec ⁡ y ∈ V ⟼ ⋃ y z ⁡ ∅ = z
4 rdgfnon ⊢ rec ⁡ y ∈ V ⟼ ⋃ y z Fn On
5 omsson ⊢ ω ⊆ On
6 peano1 ⊢ ∅ ∈ ω
7 fnfvima ⊢ rec ⁡ y ∈ V ⟼ ⋃ y z Fn On ∧ ω ⊆ On ∧ ∅ ∈ ω → rec ⁡ y ∈ V ⟼ ⋃ y z ⁡ ∅ ∈ rec ⁡ y ∈ V ⟼ ⋃ y z ω
8 4 5 6 7 mp3an ⊢ rec ⁡ y ∈ V ⟼ ⋃ y z ⁡ ∅ ∈ rec ⁡ y ∈ V ⟼ ⋃ y z ω
9 3 8 eqeltrri ⊢ z ∈ rec ⁡ y ∈ V ⟼ ⋃ y z ω
10 elunii ⊢ z ∈ z ∧ z ∈ rec ⁡ y ∈ V ⟼ ⋃ y z ω → z ∈ ⋃ rec ⁡ y ∈ V ⟼ ⋃ y z ω
11 1 9 10 mp2an ⊢ z ∈ ⋃ rec ⁡ y ∈ V ⟼ ⋃ y z ω
12 sneq ⊢ x = z → x = z
13 rdgeq2 ⊢ x = z → rec ⁡ y ∈ V ⟼ ⋃ y x = rec ⁡ y ∈ V ⟼ ⋃ y z
14 12 13 syl ⊢ x = z → rec ⁡ y ∈ V ⟼ ⋃ y x = rec ⁡ y ∈ V ⟼ ⋃ y z
15 14 imaeq1d ⊢ x = z → rec ⁡ y ∈ V ⟼ ⋃ y x ω = rec ⁡ y ∈ V ⟼ ⋃ y z ω
16 15 unieqd ⊢ x = z → ⋃ rec ⁡ y ∈ V ⟼ ⋃ y x ω = ⋃ rec ⁡ y ∈ V ⟼ ⋃ y z ω
17 16 eliuni ⊢ z ∈ A ∧ z ∈ ⋃ rec ⁡ y ∈ V ⟼ ⋃ y z ω → z ∈ ⋃ x ∈ A ⋃ rec ⁡ y ∈ V ⟼ ⋃ y x ω
18 11 17 mpan2 ⊢ z ∈ A → z ∈ ⋃ x ∈ A ⋃ rec ⁡ y ∈ V ⟼ ⋃ y x ω
19 df-ttc Could not format TC+ A = U_ x e. A U. ( rec ( ( y e. _V |-> U. y ) , { x } ) " _om ) : No typesetting found for |- TC+ A = U_ x e. A U. ( rec ( ( y e. _V |-> U. y ) , { x } ) " _om ) with typecode |-
20 18 19 eleqtrrdi Could not format ( z e. A -> z e. TC+ A ) : No typesetting found for |- ( z e. A -> z e. TC+ A ) with typecode |-
21 20 ssriv Could not format A C_ TC+ A : No typesetting found for |- A C_ TC+ A with typecode |-