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 Could not format assertion : No typesetting found for |- ( TC+ A e. _V <-> TC+ A e. U. ( R1 " On ) ) with typecode |-

Proof

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