Metamath Proof Explorer

Theorem elttcirr

Description: Irreflexivity of A e. TC+ B relationship. This is a consequence of Regularity, but it does not require Transitive Containment. We use the alternative expression dfttc4 to construct a set in which A is both e. -minimal and not e. -minimal. (Contributed by Matthew House, 6-Apr-2026)

Ref Expression
Assertion elttcirr 
|- -. A e. TC+ A

Proof

Step Hyp Ref Expression
1 vex 
 |-  y e. _V
2 inss2 
 |-  ( A i^i y ) C_ y
3 ssn0 
 |-  ( ( ( A i^i y ) C_ y /\ ( A i^i y ) =/= (/) ) -> y =/= (/) )
4 2 3 mpan 
 |-  ( ( A i^i y ) =/= (/) -> y =/= (/) )
5 zfreg 
 |-  ( ( y e. _V /\ y =/= (/) ) -> E. x e. y ( x i^i y ) = (/) )
6 1 4 5 sylancr 
 |-  ( ( A i^i y ) =/= (/) -> E. x e. y ( x i^i y ) = (/) )
7 ineq1 
 |-  ( w = x -> ( w i^i y ) = ( x i^i y ) )
8 7 eqeq1d 
 |-  ( w = x -> ( ( w i^i y ) = (/) <-> ( x i^i y ) = (/) ) )
9 ineq1 
 |-  ( x = A -> ( x i^i y ) = ( A i^i y ) )
10 9 eqeq1d 
 |-  ( x = A -> ( ( x i^i y ) = (/) <-> ( A i^i y ) = (/) ) )
11 8 10 rexraleqim 
 |-  ( ( E. x e. y ( x i^i y ) = (/) /\ A. w e. y ( ( w i^i y ) = (/) -> w = A ) ) -> ( A i^i y ) = (/) )
12 6 11 sylan 
 |-  ( ( ( A i^i y ) =/= (/) /\ A. w e. y ( ( w i^i y ) = (/) -> w = A ) ) -> ( A i^i y ) = (/) )
13 neneq 
 |-  ( ( A i^i y ) =/= (/) -> -. ( A i^i y ) = (/) )
14 13 adantr 
 |-  ( ( ( A i^i y ) =/= (/) /\ A. w e. y ( ( w i^i y ) = (/) -> w = A ) ) -> -. ( A i^i y ) = (/) )
15 12 14 pm2.65i 
 |-  -. ( ( A i^i y ) =/= (/) /\ A. w e. y ( ( w i^i y ) = (/) -> w = A ) )
16 15 nex 
 |-  -. E. y ( ( A i^i y ) =/= (/) /\ A. w e. y ( ( w i^i y ) = (/) -> w = A ) )
17 eqeq2 
 |-  ( x = A -> ( w = x <-> w = A ) )
18 17 imbi2d 
 |-  ( x = A -> ( ( ( w i^i y ) = (/) -> w = x ) <-> ( ( w i^i y ) = (/) -> w = A ) ) )
19 18 ralbidv 
 |-  ( x = A -> ( A. w e. y ( ( w i^i y ) = (/) -> w = x ) <-> A. w e. y ( ( w i^i y ) = (/) -> w = A ) ) )
20 19 anbi2d 
 |-  ( x = A -> ( ( ( A i^i y ) =/= (/) /\ A. w e. y ( ( w i^i y ) = (/) -> w = x ) ) <-> ( ( A i^i y ) =/= (/) /\ A. w e. y ( ( w i^i y ) = (/) -> w = A ) ) ) )
21 20 exbidv 
 |-  ( x = A -> ( E. y ( ( A i^i y ) =/= (/) /\ A. w e. y ( ( w i^i y ) = (/) -> w = x ) ) <-> E. y ( ( A i^i y ) =/= (/) /\ A. w e. y ( ( w i^i y ) = (/) -> w = A ) ) ) )
22 dfttc4 
 |-  TC+ A = { x | E. y ( ( A i^i y ) =/= (/) /\ A. w e. y ( ( w i^i y ) = (/) -> w = x ) ) }
23 21 22 elab2g 
 |-  ( A e. TC+ A -> ( A e. TC+ A <-> E. y ( ( A i^i y ) =/= (/) /\ A. w e. y ( ( w i^i y ) = (/) -> w = A ) ) ) )
24 23 ibi 
 |-  ( A e. TC+ A -> E. y ( ( A i^i y ) =/= (/) /\ A. w e. y ( ( w i^i y ) = (/) -> w = A ) ) )
25 16 24 mto 
 |-  -. A e. TC+ A