Metamath Proof Explorer

Theorem ttcwf2

Description: If a transitive closure class is a set, then it is well-founded, assuming Regularity. (Contributed by Matthew House, 6-Apr-2026)

Ref Expression
Assertion ttcwf2 
|- ( TC+ A e. _V <-> TC+ A e. U. ( R1 " On ) )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( x e. ( TC+ A \ U. ( R1 " On ) ) /\ ( x i^i ( TC+ A \ U. ( R1 " On ) ) ) = (/) ) -> x e. ( TC+ A \ U. ( R1 " On ) ) )
2 1 eldifad 
 |-  ( ( x e. ( TC+ A \ U. ( R1 " On ) ) /\ ( x i^i ( TC+ A \ U. ( R1 " On ) ) ) = (/) ) -> x e. TC+ A )
3 ttctr2 
 |-  ( x e. TC+ A -> x C_ TC+ A )
4 2 3 syl 
 |-  ( ( x e. ( TC+ A \ U. ( R1 " On ) ) /\ ( x i^i ( TC+ A \ U. ( R1 " On ) ) ) = (/) ) -> x C_ TC+ A )
5 dfss2 
 |-  ( x C_ TC+ A <-> ( x i^i TC+ A ) = x )
6 4 5 sylib 
 |-  ( ( x e. ( TC+ A \ U. ( R1 " On ) ) /\ ( x i^i ( TC+ A \ U. ( R1 " On ) ) ) = (/) ) -> ( x i^i TC+ A ) = x )
7 inssdif0 
 |-  ( ( x i^i TC+ A ) C_ U. ( R1 " On ) <-> ( x i^i ( TC+ A \ U. ( R1 " On ) ) ) = (/) )
8 7 bilanri 
 |-  ( ( x e. ( TC+ A \ U. ( R1 " On ) ) /\ ( x i^i ( TC+ A \ U. ( R1 " On ) ) ) = (/) ) -> ( x i^i TC+ A ) C_ U. ( R1 " On ) )
9 6 8 eqsstrrd 
 |-  ( ( x e. ( TC+ A \ U. ( R1 " On ) ) /\ ( x i^i ( TC+ A \ U. ( R1 " On ) ) ) = (/) ) -> x C_ U. ( R1 " On ) )
10 vex 
 |-  x e. _V
11 10 r1elss 
 |-  ( x e. U. ( R1 " On ) <-> x C_ U. ( R1 " On ) )
12 9 11 sylibr 
 |-  ( ( x e. ( TC+ A \ U. ( R1 " On ) ) /\ ( x i^i ( TC+ A \ U. ( R1 " On ) ) ) = (/) ) -> x e. U. ( R1 " On ) )
13 1 eldifbd 
 |-  ( ( x e. ( TC+ A \ U. ( R1 " On ) ) /\ ( x i^i ( TC+ A \ U. ( R1 " On ) ) ) = (/) ) -> -. x e. U. ( R1 " On ) )
14 12 13 pm2.65da 
 |-  ( x e. ( TC+ A \ U. ( R1 " On ) ) -> -. ( x i^i ( TC+ A \ U. ( R1 " On ) ) ) = (/) )
15 14 nrex 
 |-  -. E. x e. ( TC+ A \ U. ( R1 " On ) ) ( x i^i ( TC+ A \ U. ( R1 " On ) ) ) = (/)
16 15 a1i 
 |-  ( TC+ A e. _V -> -. E. x e. ( TC+ A \ U. ( R1 " On ) ) ( x i^i ( TC+ A \ U. ( R1 " On ) ) ) = (/) )
17 difexg 
 |-  ( TC+ A e. _V -> ( TC+ A \ U. ( R1 " On ) ) e. _V )
18 zfreg 
 |-  ( ( ( TC+ A \ U. ( R1 " On ) ) e. _V /\ ( TC+ A \ U. ( R1 " On ) ) =/= (/) ) -> E. x e. ( TC+ A \ U. ( R1 " On ) ) ( x i^i ( TC+ A \ U. ( R1 " On ) ) ) = (/) )
19 17 18 sylan 
 |-  ( ( TC+ A e. _V /\ ( TC+ A \ U. ( R1 " On ) ) =/= (/) ) -> E. x e. ( TC+ A \ U. ( R1 " On ) ) ( x i^i ( TC+ A \ U. ( R1 " On ) ) ) = (/) )
20 16 19 mtand 
 |-  ( TC+ A e. _V -> -. ( TC+ A \ U. ( R1 " On ) ) =/= (/) )
21 nne 
 |-  ( -. ( TC+ A \ U. ( R1 " On ) ) =/= (/) <-> ( TC+ A \ U. ( R1 " On ) ) = (/) )
22 20 21 sylib 
 |-  ( TC+ A e. _V -> ( TC+ A \ U. ( R1 " On ) ) = (/) )
23 ssdif0 
 |-  ( TC+ A C_ U. ( R1 " On ) <-> ( TC+ A \ U. ( R1 " On ) ) = (/) )
24 22 23 sylibr 
 |-  ( TC+ A e. _V -> TC+ A C_ U. ( R1 " On ) )
25 eleq1 
 |-  ( x = TC+ A -> ( x e. U. ( R1 " On ) <-> TC+ A e. U. ( R1 " On ) ) )
26 sseq1 
 |-  ( x = TC+ A -> ( x C_ U. ( R1 " On ) <-> TC+ A C_ U. ( R1 " On ) ) )
27 25 26 bibi12d 
 |-  ( x = TC+ A -> ( ( x e. U. ( R1 " On ) <-> x C_ U. ( R1 " On ) ) <-> ( TC+ A e. U. ( R1 " On ) <-> TC+ A C_ U. ( R1 " On ) ) ) )
28 27 11 vtoclg 
 |-  ( TC+ A e. _V -> ( TC+ A e. U. ( R1 " On ) <-> TC+ A C_ U. ( R1 " On ) ) )
29 24 28 mpbird 
 |-  ( TC+ A e. _V -> TC+ A e. U. ( R1 " On ) )
30 elex 
 |-  ( TC+ A e. U. ( R1 " On ) -> TC+ A e. _V )
31 29 30 impbii 
 |-  ( TC+ A e. _V <-> TC+ A e. U. ( R1 " On ) )