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	⊢ 𝐴 ∈ V
Assertion	tc2	⊢ ( ( TC ‘ 𝐴 ) ∪ { 𝐴 } ) = ∩ { 𝑥 ∣ ( 𝐴 ∈ 𝑥 ∧ Tr 𝑥 ) }

Proof

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