Metamath Proof Explorer

Theorem tz9.1regs

Description: Every set has a transitive closure (the smallest transitive extension). This version of tz9.1 depends on ax-regs instead of ax-reg and ax-inf2 . This suggests a possible answer to the third question posed in tz9.1 , namely that the missing property is that countably infinite classes must obey regularity. In ZF set theory we can prove this by showing that countably infinite classes are sets and thus ax-reg applies to them directly, but in a finitist context it seems that an axiom like ax-regs is required since countably infinite classes are proper classes. (Contributed by BTernaryTau, 31-Dec-2025)

Ref Expression
Hypothesis tz9.1regs.1 
|- A e. _V
Assertion tz9.1regs 
|- E. x ( A C_ x /\ Tr x /\ A. y ( ( A C_ y /\ Tr y ) -> x C_ y ) )

Proof

Step Hyp Ref Expression
1 tz9.1regs.1 
 |-  A e. _V
2 sseq1 
 |-  ( z = A -> ( z C_ x <-> A C_ x ) )
3 cleq1lem 
 |-  ( z = A -> ( ( z C_ y /\ Tr y ) <-> ( A C_ y /\ Tr y ) ) )
4 3 imbi1d 
 |-  ( z = A -> ( ( ( z C_ y /\ Tr y ) -> x C_ y ) <-> ( ( A C_ y /\ Tr y ) -> x C_ y ) ) )
5 4 albidv 
 |-  ( z = A -> ( A. y ( ( z C_ y /\ Tr y ) -> x C_ y ) <-> A. y ( ( A C_ y /\ Tr y ) -> x C_ y ) ) )
6 2 5 3anbi13d 
 |-  ( z = A -> ( ( z C_ x /\ Tr x /\ A. y ( ( z C_ y /\ Tr y ) -> x C_ y ) ) <-> ( A C_ x /\ Tr x /\ A. y ( ( A C_ y /\ Tr y ) -> x C_ y ) ) ) )
7 6 exbidv 
 |-  ( z = A -> ( E. x ( z C_ x /\ Tr x /\ A. y ( ( z C_ y /\ Tr y ) -> x C_ y ) ) <-> E. x ( A C_ x /\ Tr x /\ A. y ( ( A C_ y /\ Tr y ) -> x C_ y ) ) ) )
8 sseq1 
 |-  ( z = w -> ( z C_ x <-> w C_ x ) )
9 cleq1lem 
 |-  ( z = w -> ( ( z C_ y /\ Tr y ) <-> ( w C_ y /\ Tr y ) ) )
10 9 imbi1d 
 |-  ( z = w -> ( ( ( z C_ y /\ Tr y ) -> x C_ y ) <-> ( ( w C_ y /\ Tr y ) -> x C_ y ) ) )
11 10 albidv 
 |-  ( z = w -> ( A. y ( ( z C_ y /\ Tr y ) -> x C_ y ) <-> A. y ( ( w C_ y /\ Tr y ) -> x C_ y ) ) )
12 8 11 3anbi13d 
 |-  ( z = w -> ( ( z C_ x /\ Tr x /\ A. y ( ( z C_ y /\ Tr y ) -> x C_ y ) ) <-> ( w C_ x /\ Tr x /\ A. y ( ( w C_ y /\ Tr y ) -> x C_ y ) ) ) )
13 12 exbidv 
 |-  ( z = w -> ( E. x ( z C_ x /\ Tr x /\ A. y ( ( z C_ y /\ Tr y ) -> x C_ y ) ) <-> E. x ( w C_ x /\ Tr x /\ A. y ( ( w C_ y /\ Tr y ) -> x C_ y ) ) ) )
14 vex 
 |-  z e. _V
15 3simpa 
 |-  ( ( w C_ x /\ Tr x /\ A. y ( ( w C_ y /\ Tr y ) -> x C_ y ) ) -> ( w C_ x /\ Tr x ) )
16 15 eximi 
 |-  ( E. x ( w C_ x /\ Tr x /\ A. y ( ( w C_ y /\ Tr y ) -> x C_ y ) ) -> E. x ( w C_ x /\ Tr x ) )
17 intexab 
 |-  ( E. x ( w C_ x /\ Tr x ) <-> |^| { x | ( w C_ x /\ Tr x ) } e. _V )
18 16 17 sylib 
 |-  ( E. x ( w C_ x /\ Tr x /\ A. y ( ( w C_ y /\ Tr y ) -> x C_ y ) ) -> |^| { x | ( w C_ x /\ Tr x ) } e. _V )
19 18 ralimi 
 |-  ( A. w e. z E. x ( w C_ x /\ Tr x /\ A. y ( ( w C_ y /\ Tr y ) -> x C_ y ) ) -> A. w e. z |^| { x | ( w C_ x /\ Tr x ) } e. _V )
20 iunexg 
 |-  ( ( z e. _V /\ A. w e. z |^| { x | ( w C_ x /\ Tr x ) } e. _V ) -> U_ w e. z |^| { x | ( w C_ x /\ Tr x ) } e. _V )
21 14 19 20 sylancr 
 |-  ( A. w e. z E. x ( w C_ x /\ Tr x /\ A. y ( ( w C_ y /\ Tr y ) -> x C_ y ) ) -> U_ w e. z |^| { x | ( w C_ x /\ Tr x ) } e. _V )
22 unexg 
 |-  ( ( z e. _V /\ U_ w e. z |^| { x | ( w C_ x /\ Tr x ) } e. _V ) -> ( z u. U_ w e. z |^| { x | ( w C_ x /\ Tr x ) } ) e. _V )
23 14 21 22 sylancr 
 |-  ( A. w e. z E. x ( w C_ x /\ Tr x /\ A. y ( ( w C_ y /\ Tr y ) -> x C_ y ) ) -> ( z u. U_ w e. z |^| { x | ( w C_ x /\ Tr x ) } ) e. _V )
24 ssun1 
 |-  z C_ ( z u. U_ w e. z |^| { x | ( w C_ x /\ Tr x ) } )
25 uniun 
 |-  U. ( z u. U_ w e. z |^| { x | ( w C_ x /\ Tr x ) } ) = ( U. z u. U. U_ w e. z |^| { x | ( w C_ x /\ Tr x ) } )
26 uniiun 
 |-  U. z = U_ w e. z w
27 ssmin 
 |-  w C_ |^| { x | ( w C_ x /\ Tr x ) }
28 27 rgenw 
 |-  A. w e. z w C_ |^| { x | ( w C_ x /\ Tr x ) }
29 ss2iun 
 |-  ( A. w e. z w C_ |^| { x | ( w C_ x /\ Tr x ) } -> U_ w e. z w C_ U_ w e. z |^| { x | ( w C_ x /\ Tr x ) } )
30 28 29 ax-mp 
 |-  U_ w e. z w C_ U_ w e. z |^| { x | ( w C_ x /\ Tr x ) }
31 26 30 eqsstri 
 |-  U. z C_ U_ w e. z |^| { x | ( w C_ x /\ Tr x ) }
32 ssun4 
 |-  ( U. z C_ U_ w e. z |^| { x | ( w C_ x /\ Tr x ) } -> U. z C_ ( z u. U_ w e. z |^| { x | ( w C_ x /\ Tr x ) } ) )
33 31 32 ax-mp 
 |-  U. z C_ ( z u. U_ w e. z |^| { x | ( w C_ x /\ Tr x ) } )
34 trint 
 |-  ( A. y e. { x | ( w C_ x /\ Tr x ) } Tr y -> Tr |^| { x | ( w C_ x /\ Tr x ) } )
35 sseq2 
 |-  ( x = y -> ( w C_ x <-> w C_ y ) )
36 treq 
 |-  ( x = y -> ( Tr x <-> Tr y ) )
37 35 36 anbi12d 
 |-  ( x = y -> ( ( w C_ x /\ Tr x ) <-> ( w C_ y /\ Tr y ) ) )
38 37 cbvabv 
 |-  { x | ( w C_ x /\ Tr x ) } = { y | ( w C_ y /\ Tr y ) }
39 38 eqabri 
 |-  ( y e. { x | ( w C_ x /\ Tr x ) } <-> ( w C_ y /\ Tr y ) )
40 39 simprbi 
 |-  ( y e. { x | ( w C_ x /\ Tr x ) } -> Tr y )
41 34 40 mprg 
 |-  Tr |^| { x | ( w C_ x /\ Tr x ) }
42 41 rgenw 
 |-  A. w e. z Tr |^| { x | ( w C_ x /\ Tr x ) }
43 triun 
 |-  ( A. w e. z Tr |^| { x | ( w C_ x /\ Tr x ) } -> Tr U_ w e. z |^| { x | ( w C_ x /\ Tr x ) } )
44 42 43 ax-mp 
 |-  Tr U_ w e. z |^| { x | ( w C_ x /\ Tr x ) }
45 df-tr 
 |-  ( Tr U_ w e. z |^| { x | ( w C_ x /\ Tr x ) } <-> U. U_ w e. z |^| { x | ( w C_ x /\ Tr x ) } C_ U_ w e. z |^| { x | ( w C_ x /\ Tr x ) } )
46 44 45 mpbi 
 |-  U. U_ w e. z |^| { x | ( w C_ x /\ Tr x ) } C_ U_ w e. z |^| { x | ( w C_ x /\ Tr x ) }
47 ssun4 
 |-  ( U. U_ w e. z |^| { x | ( w C_ x /\ Tr x ) } C_ U_ w e. z |^| { x | ( w C_ x /\ Tr x ) } -> U. U_ w e. z |^| { x | ( w C_ x /\ Tr x ) } C_ ( z u. U_ w e. z |^| { x | ( w C_ x /\ Tr x ) } ) )
48 46 47 ax-mp 
 |-  U. U_ w e. z |^| { x | ( w C_ x /\ Tr x ) } C_ ( z u. U_ w e. z |^| { x | ( w C_ x /\ Tr x ) } )
49 33 48 unssi 
 |-  ( U. z u. U. U_ w e. z |^| { x | ( w C_ x /\ Tr x ) } ) C_ ( z u. U_ w e. z |^| { x | ( w C_ x /\ Tr x ) } )
50 25 49 eqsstri 
 |-  U. ( z u. U_ w e. z |^| { x | ( w C_ x /\ Tr x ) } ) C_ ( z u. U_ w e. z |^| { x | ( w C_ x /\ Tr x ) } )
51 df-tr 
 |-  ( Tr ( z u. U_ w e. z |^| { x | ( w C_ x /\ Tr x ) } ) <-> U. ( z u. U_ w e. z |^| { x | ( w C_ x /\ Tr x ) } ) C_ ( z u. U_ w e. z |^| { x | ( w C_ x /\ Tr x ) } ) )
52 50 51 mpbir 
 |-  Tr ( z u. U_ w e. z |^| { x | ( w C_ x /\ Tr x ) } )
53 ssel 
 |-  ( z C_ y -> ( w e. z -> w e. y ) )
54 trss 
 |-  ( Tr y -> ( w e. y -> w C_ y ) )
55 53 54 sylan9 
 |-  ( ( z C_ y /\ Tr y ) -> ( w e. z -> w C_ y ) )
56 simpr 
 |-  ( ( z C_ y /\ Tr y ) -> Tr y )
57 55 56 jctird 
 |-  ( ( z C_ y /\ Tr y ) -> ( w e. z -> ( w C_ y /\ Tr y ) ) )
58 rabab 
 |-  { x e. _V | ( w C_ x /\ Tr x ) } = { x | ( w C_ x /\ Tr x ) }
59 58 inteqi 
 |-  |^| { x e. _V | ( w C_ x /\ Tr x ) } = |^| { x | ( w C_ x /\ Tr x ) }
60 vex 
 |-  y e. _V
61 37 intminss 
 |-  ( ( y e. _V /\ ( w C_ y /\ Tr y ) ) -> |^| { x e. _V | ( w C_ x /\ Tr x ) } C_ y )
62 60 61 mpan 
 |-  ( ( w C_ y /\ Tr y ) -> |^| { x e. _V | ( w C_ x /\ Tr x ) } C_ y )
63 59 62 eqsstrrid 
 |-  ( ( w C_ y /\ Tr y ) -> |^| { x | ( w C_ x /\ Tr x ) } C_ y )
64 57 63 syl6 
 |-  ( ( z C_ y /\ Tr y ) -> ( w e. z -> |^| { x | ( w C_ x /\ Tr x ) } C_ y ) )
65 64 ralrimiv 
 |-  ( ( z C_ y /\ Tr y ) -> A. w e. z |^| { x | ( w C_ x /\ Tr x ) } C_ y )
66 iunss 
 |-  ( U_ w e. z |^| { x | ( w C_ x /\ Tr x ) } C_ y <-> A. w e. z |^| { x | ( w C_ x /\ Tr x ) } C_ y )
67 65 66 sylibr 
 |-  ( ( z C_ y /\ Tr y ) -> U_ w e. z |^| { x | ( w C_ x /\ Tr x ) } C_ y )
68 unss 
 |-  ( ( z C_ y /\ U_ w e. z |^| { x | ( w C_ x /\ Tr x ) } C_ y ) <-> ( z u. U_ w e. z |^| { x | ( w C_ x /\ Tr x ) } ) C_ y )
69 68 biimpi 
 |-  ( ( z C_ y /\ U_ w e. z |^| { x | ( w C_ x /\ Tr x ) } C_ y ) -> ( z u. U_ w e. z |^| { x | ( w C_ x /\ Tr x ) } ) C_ y )
70 67 69 syldan 
 |-  ( ( z C_ y /\ Tr y ) -> ( z u. U_ w e. z |^| { x | ( w C_ x /\ Tr x ) } ) C_ y )
71 70 ax-gen 
 |-  A. y ( ( z C_ y /\ Tr y ) -> ( z u. U_ w e. z |^| { x | ( w C_ x /\ Tr x ) } ) C_ y )
72 24 52 71 3pm3.2i 
 |-  ( z C_ ( z u. U_ w e. z |^| { x | ( w C_ x /\ Tr x ) } ) /\ Tr ( z u. U_ w e. z |^| { x | ( w C_ x /\ Tr x ) } ) /\ A. y ( ( z C_ y /\ Tr y ) -> ( z u. U_ w e. z |^| { x | ( w C_ x /\ Tr x ) } ) C_ y ) )
73 sseq2 
 |-  ( u = ( z u. U_ w e. z |^| { x | ( w C_ x /\ Tr x ) } ) -> ( z C_ u <-> z C_ ( z u. U_ w e. z |^| { x | ( w C_ x /\ Tr x ) } ) ) )
74 treq 
 |-  ( u = ( z u. U_ w e. z |^| { x | ( w C_ x /\ Tr x ) } ) -> ( Tr u <-> Tr ( z u. U_ w e. z |^| { x | ( w C_ x /\ Tr x ) } ) ) )
75 sseq1 
 |-  ( u = ( z u. U_ w e. z |^| { x | ( w C_ x /\ Tr x ) } ) -> ( u C_ y <-> ( z u. U_ w e. z |^| { x | ( w C_ x /\ Tr x ) } ) C_ y ) )
76 75 imbi2d 
 |-  ( u = ( z u. U_ w e. z |^| { x | ( w C_ x /\ Tr x ) } ) -> ( ( ( z C_ y /\ Tr y ) -> u C_ y ) <-> ( ( z C_ y /\ Tr y ) -> ( z u. U_ w e. z |^| { x | ( w C_ x /\ Tr x ) } ) C_ y ) ) )
77 76 albidv 
 |-  ( u = ( z u. U_ w e. z |^| { x | ( w C_ x /\ Tr x ) } ) -> ( A. y ( ( z C_ y /\ Tr y ) -> u C_ y ) <-> A. y ( ( z C_ y /\ Tr y ) -> ( z u. U_ w e. z |^| { x | ( w C_ x /\ Tr x ) } ) C_ y ) ) )
78 73 74 77 3anbi123d 
 |-  ( u = ( z u. U_ w e. z |^| { x | ( w C_ x /\ Tr x ) } ) -> ( ( z C_ u /\ Tr u /\ A. y ( ( z C_ y /\ Tr y ) -> u C_ y ) ) <-> ( z C_ ( z u. U_ w e. z |^| { x | ( w C_ x /\ Tr x ) } ) /\ Tr ( z u. U_ w e. z |^| { x | ( w C_ x /\ Tr x ) } ) /\ A. y ( ( z C_ y /\ Tr y ) -> ( z u. U_ w e. z |^| { x | ( w C_ x /\ Tr x ) } ) C_ y ) ) ) )
79 78 spcegv 
 |-  ( ( z u. U_ w e. z |^| { x | ( w C_ x /\ Tr x ) } ) e. _V -> ( ( z C_ ( z u. U_ w e. z |^| { x | ( w C_ x /\ Tr x ) } ) /\ Tr ( z u. U_ w e. z |^| { x | ( w C_ x /\ Tr x ) } ) /\ A. y ( ( z C_ y /\ Tr y ) -> ( z u. U_ w e. z |^| { x | ( w C_ x /\ Tr x ) } ) C_ y ) ) -> E. u ( z C_ u /\ Tr u /\ A. y ( ( z C_ y /\ Tr y ) -> u C_ y ) ) ) )
80 sseq2 
 |-  ( u = x -> ( z C_ u <-> z C_ x ) )
81 treq 
 |-  ( u = x -> ( Tr u <-> Tr x ) )
82 sseq1 
 |-  ( u = x -> ( u C_ y <-> x C_ y ) )
83 82 imbi2d 
 |-  ( u = x -> ( ( ( z C_ y /\ Tr y ) -> u C_ y ) <-> ( ( z C_ y /\ Tr y ) -> x C_ y ) ) )
84 83 albidv 
 |-  ( u = x -> ( A. y ( ( z C_ y /\ Tr y ) -> u C_ y ) <-> A. y ( ( z C_ y /\ Tr y ) -> x C_ y ) ) )
85 80 81 84 3anbi123d 
 |-  ( u = x -> ( ( z C_ u /\ Tr u /\ A. y ( ( z C_ y /\ Tr y ) -> u C_ y ) ) <-> ( z C_ x /\ Tr x /\ A. y ( ( z C_ y /\ Tr y ) -> x C_ y ) ) ) )
86 85 cbvexvw 
 |-  ( E. u ( z C_ u /\ Tr u /\ A. y ( ( z C_ y /\ Tr y ) -> u C_ y ) ) <-> E. x ( z C_ x /\ Tr x /\ A. y ( ( z C_ y /\ Tr y ) -> x C_ y ) ) )
87 79 86 imbitrdi 
 |-  ( ( z u. U_ w e. z |^| { x | ( w C_ x /\ Tr x ) } ) e. _V -> ( ( z C_ ( z u. U_ w e. z |^| { x | ( w C_ x /\ Tr x ) } ) /\ Tr ( z u. U_ w e. z |^| { x | ( w C_ x /\ Tr x ) } ) /\ A. y ( ( z C_ y /\ Tr y ) -> ( z u. U_ w e. z |^| { x | ( w C_ x /\ Tr x ) } ) C_ y ) ) -> E. x ( z C_ x /\ Tr x /\ A. y ( ( z C_ y /\ Tr y ) -> x C_ y ) ) ) )
88 23 72 87 mpisyl 
 |-  ( A. w e. z E. x ( w C_ x /\ Tr x /\ A. y ( ( w C_ y /\ Tr y ) -> x C_ y ) ) -> E. x ( z C_ x /\ Tr x /\ A. y ( ( z C_ y /\ Tr y ) -> x C_ y ) ) )
89 13 88 setinds2regs 
 |-  E. x ( z C_ x /\ Tr x /\ A. y ( ( z C_ y /\ Tr y ) -> x C_ y ) )
90 1 7 89 vtocl 
 |-  E. x ( A C_ x /\ Tr x /\ A. y ( ( A C_ y /\ Tr y ) -> x C_ y ) )