Metamath Proof Explorer

Theorem tc2

Description: A variant of the definition of the transitive closure function, using instead the smallest transitive set containing A as a member, gives almost the same set, except that A itself must be added because it is not usually a member of ( TCA ) (and it is never a member if A is well-founded). (Contributed by Mario Carneiro, 23-Jun-2013)

Ref Expression
Hypothesis tc2.1 ⊢A∈V
Assertion tc2 ⊢TC⁡A∪A=⋂x|A∈x∧Tr⁡x

Proof

Step Hyp Ref Expression
1 tc2.1 ⊢A∈V
2 tcvalg ⊢A∈V→TC⁡A=⋂x|A⊆x∧Tr⁡x
3 1 2 ax-mp ⊢TC⁡A=⋂x|A⊆x∧Tr⁡x
4 trss ⊢Tr⁡x→A∈x→A⊆x
5 4 imdistanri ⊢A∈x∧Tr⁡x→A⊆x∧Tr⁡x
6 5 ss2abi ⊢x|A∈x∧Tr⁡x⊆x|A⊆x∧Tr⁡x
7 intss ⊢x|A∈x∧Tr⁡x⊆x|A⊆x∧Tr⁡x→⋂x|A⊆x∧Tr⁡x⊆⋂x|A∈x∧Tr⁡x
8 6 7 ax-mp ⊢⋂x|A⊆x∧Tr⁡x⊆⋂x|A∈x∧Tr⁡x
9 3 8 eqsstri ⊢TC⁡A⊆⋂x|A∈x∧Tr⁡x
10 1 elintab ⊢A∈⋂x|A∈x∧Tr⁡x↔∀xA∈x∧Tr⁡x→A∈x
11 simpl ⊢A∈x∧Tr⁡x→A∈x
12 10 11 mpgbir ⊢A∈⋂x|A∈x∧Tr⁡x
13 1 snss ⊢A∈⋂x|A∈x∧Tr⁡x↔A⊆⋂x|A∈x∧Tr⁡x
14 12 13 mpbi ⊢A⊆⋂x|A∈x∧Tr⁡x
15 9 14 unssi ⊢TC⁡A∪A⊆⋂x|A∈x∧Tr⁡x
16 1 snid ⊢A∈A
17 elun2 ⊢A∈A→A∈TC⁡A∪A
18 16 17 ax-mp ⊢A∈TC⁡A∪A
19 uniun ⊢⋃TC⁡A∪A=⋃TC⁡A∪⋃A
20 tctr ⊢Tr⁡TC⁡A
21 df-tr ⊢Tr⁡TC⁡A↔⋃TC⁡A⊆TC⁡A
22 20 21 mpbi ⊢⋃TC⁡A⊆TC⁡A
23 1 unisn ⊢⋃A=A
24 tcid ⊢A∈V→A⊆TC⁡A
25 1 24 ax-mp ⊢A⊆TC⁡A
26 23 25 eqsstri ⊢⋃A⊆TC⁡A
27 22 26 unssi ⊢⋃TC⁡A∪⋃A⊆TC⁡A
28 19 27 eqsstri ⊢⋃TC⁡A∪A⊆TC⁡A
29 ssun1 ⊢TC⁡A⊆TC⁡A∪A
30 28 29 sstri ⊢⋃TC⁡A∪A⊆TC⁡A∪A
31 df-tr ⊢Tr⁡TC⁡A∪A↔⋃TC⁡A∪A⊆TC⁡A∪A
32 30 31 mpbir ⊢Tr⁡TC⁡A∪A
33 fvex ⊢TC⁡A∈V
34 snex ⊢A∈V
35 33 34 unex ⊢TC⁡A∪A∈V
36 eleq2 ⊢x=TC⁡A∪A→A∈x↔A∈TC⁡A∪A
37 treq ⊢x=TC⁡A∪A→Tr⁡x↔Tr⁡TC⁡A∪A
38 36 37 anbi12d ⊢x=TC⁡A∪A→A∈x∧Tr⁡x↔A∈TC⁡A∪A∧Tr⁡TC⁡A∪A
39 35 38 elab ⊢TC⁡A∪A∈x|A∈x∧Tr⁡x↔A∈TC⁡A∪A∧Tr⁡TC⁡A∪A
40 18 32 39 mpbir2an ⊢TC⁡A∪A∈x|A∈x∧Tr⁡x
41 intss1 ⊢TC⁡A∪A∈x|A∈x∧Tr⁡x→⋂x|A∈x∧Tr⁡x⊆TC⁡A∪A
42 40 41 ax-mp ⊢⋂x|A∈x∧Tr⁡x⊆TC⁡A∪A
43 15 42 eqssi ⊢TC⁡A∪A=⋂x|A∈x∧Tr⁡x