Metamath Proof Explorer

Theorem dfttc4

Description: An alternative expression for the transitive closure of a class, assuming Regularity. A set x is contained in the transitive closure of A iff we can construct an e. -chain from x to an element of A . This weak definition is primarily useful for proving elttcirr . (Contributed by Matthew House, 6-Apr-2026)

Ref Expression
Assertion dfttc4 
|- TC+ A = { x | E. y ( ( A i^i y ) =/= (/) /\ A. z e. y ( ( z i^i y ) = (/) -> z = x ) ) }

Proof

Step Hyp Ref Expression
1 eqid 
 |-  { x | E. y ( ( A i^i y ) =/= (/) /\ A. z e. y ( ( z i^i y ) = (/) -> z = x ) ) } = { x | E. y ( ( A i^i y ) =/= (/) /\ A. z e. y ( ( z i^i y ) = (/) -> z = x ) ) }
2 1 dfttc4lem2 
 |-  ( A C_ { x | E. y ( ( A i^i y ) =/= (/) /\ A. z e. y ( ( z i^i y ) = (/) -> z = x ) ) } /\ Tr { x | E. y ( ( A i^i y ) =/= (/) /\ A. z e. y ( ( z i^i y ) = (/) -> z = x ) ) } )
3 ttcmin 
 |-  ( ( A C_ { x | E. y ( ( A i^i y ) =/= (/) /\ A. z e. y ( ( z i^i y ) = (/) -> z = x ) ) } /\ Tr { x | E. y ( ( A i^i y ) =/= (/) /\ A. z e. y ( ( z i^i y ) = (/) -> z = x ) ) } ) -> TC+ A C_ { x | E. y ( ( A i^i y ) =/= (/) /\ A. z e. y ( ( z i^i y ) = (/) -> z = x ) ) } )
4 2 3 ax-mp 
 |-  TC+ A C_ { x | E. y ( ( A i^i y ) =/= (/) /\ A. z e. y ( ( z i^i y ) = (/) -> z = x ) ) }
5 vex 
 |-  w e. _V
6 equequ2 
 |-  ( x = w -> ( z = x <-> z = w ) )
7 6 imbi2d 
 |-  ( x = w -> ( ( ( z i^i y ) = (/) -> z = x ) <-> ( ( z i^i y ) = (/) -> z = w ) ) )
8 7 ralbidv 
 |-  ( x = w -> ( A. z e. y ( ( z i^i y ) = (/) -> z = x ) <-> A. z e. y ( ( z i^i y ) = (/) -> z = w ) ) )
9 8 anbi2d 
 |-  ( x = w -> ( ( ( A i^i y ) =/= (/) /\ A. z e. y ( ( z i^i y ) = (/) -> z = x ) ) <-> ( ( A i^i y ) =/= (/) /\ A. z e. y ( ( z i^i y ) = (/) -> z = w ) ) ) )
10 9 exbidv 
 |-  ( x = w -> ( E. y ( ( A i^i y ) =/= (/) /\ A. z e. y ( ( z i^i y ) = (/) -> z = x ) ) <-> E. y ( ( A i^i y ) =/= (/) /\ A. z e. y ( ( z i^i y ) = (/) -> z = w ) ) ) )
11 5 10 elab 
 |-  ( w e. { x | E. y ( ( A i^i y ) =/= (/) /\ A. z e. y ( ( z i^i y ) = (/) -> z = x ) ) } <-> E. y ( ( A i^i y ) =/= (/) /\ A. z e. y ( ( z i^i y ) = (/) -> z = w ) ) )
12 vex 
 |-  y e. _V
13 12 inex2 
 |-  ( TC+ A i^i y ) e. _V
14 ttcid 
 |-  A C_ TC+ A
15 ssrin 
 |-  ( A C_ TC+ A -> ( A i^i y ) C_ ( TC+ A i^i y ) )
16 14 15 ax-mp 
 |-  ( A i^i y ) C_ ( TC+ A i^i y )
17 ssn0 
 |-  ( ( ( A i^i y ) C_ ( TC+ A i^i y ) /\ ( A i^i y ) =/= (/) ) -> ( TC+ A i^i y ) =/= (/) )
18 16 17 mpan 
 |-  ( ( A i^i y ) =/= (/) -> ( TC+ A i^i y ) =/= (/) )
19 zfreg 
 |-  ( ( ( TC+ A i^i y ) e. _V /\ ( TC+ A i^i y ) =/= (/) ) -> E. x e. ( TC+ A i^i y ) ( x i^i ( TC+ A i^i y ) ) = (/) )
20 13 18 19 sylancr 
 |-  ( ( A i^i y ) =/= (/) -> E. x e. ( TC+ A i^i y ) ( x i^i ( TC+ A i^i y ) ) = (/) )
21 simpl 
 |-  ( ( x e. ( TC+ A i^i y ) /\ ( x i^i ( TC+ A i^i y ) ) = (/) ) -> x e. ( TC+ A i^i y ) )
22 21 elin2d 
 |-  ( ( x e. ( TC+ A i^i y ) /\ ( x i^i ( TC+ A i^i y ) ) = (/) ) -> x e. y )
23 inass 
 |-  ( ( x i^i TC+ A ) i^i y ) = ( x i^i ( TC+ A i^i y ) )
24 elinel1 
 |-  ( x e. ( TC+ A i^i y ) -> x e. TC+ A )
25 ttctr2 
 |-  ( x e. TC+ A -> x C_ TC+ A )
26 24 25 syl 
 |-  ( x e. ( TC+ A i^i y ) -> x C_ TC+ A )
27 dfss2 
 |-  ( x C_ TC+ A <-> ( x i^i TC+ A ) = x )
28 26 27 sylib 
 |-  ( x e. ( TC+ A i^i y ) -> ( x i^i TC+ A ) = x )
29 28 ineq1d 
 |-  ( x e. ( TC+ A i^i y ) -> ( ( x i^i TC+ A ) i^i y ) = ( x i^i y ) )
30 23 29 eqtr3id 
 |-  ( x e. ( TC+ A i^i y ) -> ( x i^i ( TC+ A i^i y ) ) = ( x i^i y ) )
31 30 eqeq1d 
 |-  ( x e. ( TC+ A i^i y ) -> ( ( x i^i ( TC+ A i^i y ) ) = (/) <-> ( x i^i y ) = (/) ) )
32 31 biimpa 
 |-  ( ( x e. ( TC+ A i^i y ) /\ ( x i^i ( TC+ A i^i y ) ) = (/) ) -> ( x i^i y ) = (/) )
33 ineq1 
 |-  ( z = x -> ( z i^i y ) = ( x i^i y ) )
34 33 eqeq1d 
 |-  ( z = x -> ( ( z i^i y ) = (/) <-> ( x i^i y ) = (/) ) )
35 equequ1 
 |-  ( z = x -> ( z = w <-> x = w ) )
36 34 35 imbi12d 
 |-  ( z = x -> ( ( ( z i^i y ) = (/) -> z = w ) <-> ( ( x i^i y ) = (/) -> x = w ) ) )
37 36 rspcv 
 |-  ( x e. y -> ( A. z e. y ( ( z i^i y ) = (/) -> z = w ) -> ( ( x i^i y ) = (/) -> x = w ) ) )
38 37 com23 
 |-  ( x e. y -> ( ( x i^i y ) = (/) -> ( A. z e. y ( ( z i^i y ) = (/) -> z = w ) -> x = w ) ) )
39 22 32 38 sylc 
 |-  ( ( x e. ( TC+ A i^i y ) /\ ( x i^i ( TC+ A i^i y ) ) = (/) ) -> ( A. z e. y ( ( z i^i y ) = (/) -> z = w ) -> x = w ) )
40 39 com12 
 |-  ( A. z e. y ( ( z i^i y ) = (/) -> z = w ) -> ( ( x e. ( TC+ A i^i y ) /\ ( x i^i ( TC+ A i^i y ) ) = (/) ) -> x = w ) )
41 eleq1w 
 |-  ( x = w -> ( x e. ( TC+ A i^i y ) <-> w e. ( TC+ A i^i y ) ) )
42 41 biimpcd 
 |-  ( x e. ( TC+ A i^i y ) -> ( x = w -> w e. ( TC+ A i^i y ) ) )
43 42 adantr 
 |-  ( ( x e. ( TC+ A i^i y ) /\ ( x i^i ( TC+ A i^i y ) ) = (/) ) -> ( x = w -> w e. ( TC+ A i^i y ) ) )
44 40 43 sylcom 
 |-  ( A. z e. y ( ( z i^i y ) = (/) -> z = w ) -> ( ( x e. ( TC+ A i^i y ) /\ ( x i^i ( TC+ A i^i y ) ) = (/) ) -> w e. ( TC+ A i^i y ) ) )
45 44 imp 
 |-  ( ( A. z e. y ( ( z i^i y ) = (/) -> z = w ) /\ ( x e. ( TC+ A i^i y ) /\ ( x i^i ( TC+ A i^i y ) ) = (/) ) ) -> w e. ( TC+ A i^i y ) )
46 45 rexlimdvaa 
 |-  ( A. z e. y ( ( z i^i y ) = (/) -> z = w ) -> ( E. x e. ( TC+ A i^i y ) ( x i^i ( TC+ A i^i y ) ) = (/) -> w e. ( TC+ A i^i y ) ) )
47 20 46 mpan9 
 |-  ( ( ( A i^i y ) =/= (/) /\ A. z e. y ( ( z i^i y ) = (/) -> z = w ) ) -> w e. ( TC+ A i^i y ) )
48 47 elin1d 
 |-  ( ( ( A i^i y ) =/= (/) /\ A. z e. y ( ( z i^i y ) = (/) -> z = w ) ) -> w e. TC+ A )
49 48 exlimiv 
 |-  ( E. y ( ( A i^i y ) =/= (/) /\ A. z e. y ( ( z i^i y ) = (/) -> z = w ) ) -> w e. TC+ A )
50 11 49 sylbi 
 |-  ( w e. { x | E. y ( ( A i^i y ) =/= (/) /\ A. z e. y ( ( z i^i y ) = (/) -> z = x ) ) } -> w e. TC+ A )
51 50 ssriv 
 |-  { x | E. y ( ( A i^i y ) =/= (/) /\ A. z e. y ( ( z i^i y ) = (/) -> z = x ) ) } C_ TC+ A
52 4 51 eqssi 
 |-  TC+ A = { x | E. y ( ( A i^i y ) =/= (/) /\ A. z e. y ( ( z i^i y ) = (/) -> z = x ) ) }