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.

A related candidate for the missing property is the non-existence of infinite descending e. -chains, proven as noinfep using ax-reg and ax-inf2 and as noinfepregs using ax-regs . If all sets are finite, then the existence of such a chain implies there is a set which does not have a transitive closure, as shown in fineqvinfep . (Contributed by BTernaryTau, 31-Dec-2025)

		Ref	Expression
	Hypothesis	tz9.1regs.1	$⊢ A \in V$
	Assertion	tz9.1regs	$⊢ \exists x (A \subseteq x \land Tr x \land \forall y ((A \subseteq y \land Tr y) \to x \subseteq y))$

Proof

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

Metamath Proof Explorer

Theorem tz9.1regs

Proof