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 simpr 
 |-  ( ( x e. ( TC+ A \ U. ( R1 " On ) ) /\ ( x i^i ( TC+ A \ U. ( R1 " On ) ) ) = (/) ) -> ( x i^i ( TC+ A \ U. ( R1 " On ) ) ) = (/) )
8 inssdif0 
 |-  ( ( x i^i TC+ A ) C_ U. ( R1 " On ) <-> ( x i^i ( TC+ A \ U. ( R1 " On ) ) ) = (/) )
9 7 8 sylibr 
 |-  ( ( x e. ( TC+ A \ U. ( R1 " On ) ) /\ ( x i^i ( TC+ A \ U. ( R1 " On ) ) ) = (/) ) -> ( x i^i TC+ A ) C_ U. ( R1 " On ) )
10 6 9 eqsstrrd 
 |-  ( ( x e. ( TC+ A \ U. ( R1 " On ) ) /\ ( x i^i ( TC+ A \ U. ( R1 " On ) ) ) = (/) ) -> x C_ U. ( R1 " On ) )
11 vex 
 |-  x e. _V
12 11 r1elss 
 |-  ( x e. U. ( R1 " On ) <-> x C_ U. ( R1 " On ) )
13 10 12 sylibr 
 |-  ( ( x e. ( TC+ A \ U. ( R1 " On ) ) /\ ( x i^i ( TC+ A \ U. ( R1 " On ) ) ) = (/) ) -> x e. U. ( R1 " On ) )
14 1 eldifbd 
 |-  ( ( x e. ( TC+ A \ U. ( R1 " On ) ) /\ ( x i^i ( TC+ A \ U. ( R1 " On ) ) ) = (/) ) -> -. x e. U. ( R1 " On ) )
15 13 14 pm2.65da 
 |-  ( x e. ( TC+ A \ U. ( R1 " On ) ) -> -. ( x i^i ( TC+ A \ U. ( R1 " On ) ) ) = (/) )
16 15 nrex 
 |-  -. E. x e. ( TC+ A \ U. ( R1 " On ) ) ( x i^i ( TC+ A \ U. ( R1 " On ) ) ) = (/)
17 16 a1i 
 |-  ( TC+ A e. _V -> -. E. x e. ( TC+ A \ U. ( R1 " On ) ) ( x i^i ( TC+ A \ U. ( R1 " On ) ) ) = (/) )
18 difexg 
 |-  ( TC+ A e. _V -> ( TC+ A \ U. ( R1 " On ) ) e. _V )
19 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 ) ) ) = (/) )
20 18 19 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 ) ) ) = (/) )
21 17 20 mtand 
 |-  ( TC+ A e. _V -> -. ( TC+ A \ U. ( R1 " On ) ) =/= (/) )
22 nne 
 |-  ( -. ( TC+ A \ U. ( R1 " On ) ) =/= (/) <-> ( TC+ A \ U. ( R1 " On ) ) = (/) )
23 21 22 sylib 
 |-  ( TC+ A e. _V -> ( TC+ A \ U. ( R1 " On ) ) = (/) )
24 ssdif0 
 |-  ( TC+ A C_ U. ( R1 " On ) <-> ( TC+ A \ U. ( R1 " On ) ) = (/) )
25 23 24 sylibr 
 |-  ( TC+ A e. _V -> TC+ A C_ U. ( R1 " On ) )
26 eleq1 
 |-  ( x = TC+ A -> ( x e. U. ( R1 " On ) <-> TC+ A e. U. ( R1 " On ) ) )
27 sseq1 
 |-  ( x = TC+ A -> ( x C_ U. ( R1 " On ) <-> TC+ A C_ U. ( R1 " On ) ) )
28 26 27 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 ) ) ) )
29 28 12 vtoclg 
 |-  ( TC+ A e. _V -> ( TC+ A e. U. ( R1 " On ) <-> TC+ A C_ U. ( R1 " On ) ) )
30 25 29 mpbird 
 |-  ( TC+ A e. _V -> TC+ A e. U. ( R1 " On ) )
31 elex 
 |-  ( TC+ A e. U. ( R1 " On ) -> TC+ A e. _V )
32 30 31 impbii 
 |-  ( TC+ A e. _V <-> TC+ A e. U. ( R1 " On ) )