Theorem tz9.1regs 35375

Description: Every set has a transitive closure (the smallest transitive extension). This version of tz9.1 9670 depends on ax-regs 35367 instead of ax-reg 9526 and ax-inf2 9582. This suggests a possible answer to the third question posed in tz9.1 9670, 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 9526 applies to them directly, but in a finitist context it seems that an axiom like ax-regs 35367 is required since countably infinite classes are proper classes.

A related candidate for the missing property is the non-existence of infinite descending ∈-chains, proven as noinfep 9601 using ax-reg 9526 and ax-inf2 9582 and as noinfepregs 35374 using ax-regs 35367. 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 35366. (Contributed by BTernaryTau, 31-Dec-2025.)

Hypothesis

Ref	Expression
tz9.1regs.1	⊢ 𝐴 ∈ V

Assertion

Ref	Expression
tz9.1regs	⊢ ∃𝑥(𝐴 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀𝑦((𝐴 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦))

Distinct variable group:   𝑥,𝐴,𝑦

Proof of Theorem tz9.1regs

Dummy variables 𝑧 𝑤 𝑢 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		tz9.1regs.1	. 2 ⊢ 𝐴 ∈ V
2		sseq1 3952	. . . 4 ⊢ (𝑧 = 𝐴 → (𝑧 ⊆ 𝑥 ↔ 𝐴 ⊆ 𝑥))
3		cleq1lem 14981	. . . . . 6 ⊢ (𝑧 = 𝐴 → ((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) ↔ (𝐴 ⊆ 𝑦 ∧ Tr 𝑦)))
4	3	imbi1d 343	. . . . 5 ⊢ (𝑧 = 𝐴 → (((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦) ↔ ((𝐴 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦)))
5	4	albidv 1930	. . . 4 ⊢ (𝑧 = 𝐴 → (∀𝑦((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦) ↔ ∀𝑦((𝐴 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦)))
6	2, 5	3anbi13d 1449	. . 3 ⊢ (𝑧 = 𝐴 → ((𝑧 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀𝑦((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦)) ↔ (𝐴 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀𝑦((𝐴 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦))))
7	6	exbidv 1931	. 2 ⊢ (𝑧 = 𝐴 → (∃𝑥(𝑧 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀𝑦((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦)) ↔ ∃𝑥(𝐴 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀𝑦((𝐴 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦))))
8		sseq1 3952	. . . . 5 ⊢ (𝑧 = 𝑤 → (𝑧 ⊆ 𝑥 ↔ 𝑤 ⊆ 𝑥))
9		cleq1lem 14981	. . . . . . 7 ⊢ (𝑧 = 𝑤 → ((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) ↔ (𝑤 ⊆ 𝑦 ∧ Tr 𝑦)))
10	9	imbi1d 343	. . . . . 6 ⊢ (𝑧 = 𝑤 → (((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦) ↔ ((𝑤 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦)))
11	10	albidv 1930	. . . . 5 ⊢ (𝑧 = 𝑤 → (∀𝑦((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦) ↔ ∀𝑦((𝑤 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦)))
12	8, 11	3anbi13d 1449	. . . 4 ⊢ (𝑧 = 𝑤 → ((𝑧 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀𝑦((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦)) ↔ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀𝑦((𝑤 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦))))
13	12	exbidv 1931	. . 3 ⊢ (𝑧 = 𝑤 → (∃𝑥(𝑧 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀𝑦((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦)) ↔ ∃𝑥(𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀𝑦((𝑤 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦))))
14		vex 3448	. . . . 5 ⊢ 𝑧 ∈ V
15		3simpa 1157	. . . . . . . . 9 ⊢ ((𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀𝑦((𝑤 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦)) → (𝑤 ⊆ 𝑥 ∧ Tr 𝑥))
16	15	eximi 1845	. . . . . . . 8 ⊢ (∃𝑥(𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀𝑦((𝑤 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦)) → ∃𝑥(𝑤 ⊆ 𝑥 ∧ Tr 𝑥))
17		intexab 5292	. . . . . . . 8 ⊢ (∃𝑥(𝑤 ⊆ 𝑥 ∧ Tr 𝑥) ↔ ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} ∈ V)
18	16, 17	sylib 220	. . . . . . 7 ⊢ (∃𝑥(𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀𝑦((𝑤 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦)) → ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} ∈ V)
19	18	ralimi 3089	. . . . . 6 ⊢ (∀𝑤 ∈ 𝑧 ∃𝑥(𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀𝑦((𝑤 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦)) → ∀𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} ∈ V)
20		iunexg 7929	. . . . . 6 ⊢ ((𝑧 ∈ V ∧ ∀𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} ∈ V) → ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} ∈ V)
21	14, 19, 20	sylancr 595	. . . . 5 ⊢ (∀𝑤 ∈ 𝑧 ∃𝑥(𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀𝑦((𝑤 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦)) → ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} ∈ V)
22		unexg 7711	. . . . 5 ⊢ ((𝑧 ∈ V ∧ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} ∈ V) → (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) ∈ V)
23	14, 21, 22	sylancr 595	. . . 4 ⊢ (∀𝑤 ∈ 𝑧 ∃𝑥(𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀𝑦((𝑤 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦)) → (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) ∈ V)
24		ssun1 4121	. . . . 5 ⊢ 𝑧 ⊆ (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)})
25		uniun 4878	. . . . . . 7 ⊢ ∪ (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) = (∪ 𝑧 ∪ ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)})
26		uniiun 5006	. . . . . . . . . 10 ⊢ ∪ 𝑧 = ∪ 𝑤 ∈ 𝑧 𝑤
27		ssmin 4915	. . . . . . . . . . . 12 ⊢ 𝑤 ⊆ ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}
28	27	rgenw 3070	. . . . . . . . . . 11 ⊢ ∀𝑤 ∈ 𝑧 𝑤 ⊆ ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}
29		ss2iun 4958	. . . . . . . . . . 11 ⊢ (∀𝑤 ∈ 𝑧 𝑤 ⊆ ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} → ∪ 𝑤 ∈ 𝑧 𝑤 ⊆ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)})
30	28, 29	ax-mp 5	. . . . . . . . . 10 ⊢ ∪ 𝑤 ∈ 𝑧 𝑤 ⊆ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}
31	26, 30	eqsstri 3973	. . . . . . . . 9 ⊢ ∪ 𝑧 ⊆ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}
32		ssun4 4124	. . . . . . . . 9 ⊢ (∪ 𝑧 ⊆ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} → ∪ 𝑧 ⊆ (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}))
33	31, 32	ax-mp 5	. . . . . . . 8 ⊢ ∪ 𝑧 ⊆ (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)})
34		trint 5215	. . . . . . . . . . . . 13 ⊢ (∀𝑦 ∈ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}Tr 𝑦 → Tr ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)})
35		sseq2 3953	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑦 → (𝑤 ⊆ 𝑥 ↔ 𝑤 ⊆ 𝑦))
36		treq 5204	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑦 → (Tr 𝑥 ↔ Tr 𝑦))
37	35, 36	anbi12d 640	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑦 → ((𝑤 ⊆ 𝑥 ∧ Tr 𝑥) ↔ (𝑤 ⊆ 𝑦 ∧ Tr 𝑦)))
38	37	cbvabv 2822	. . . . . . . . . . . . . . 15 ⊢ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} = {𝑦 ∣ (𝑤 ⊆ 𝑦 ∧ Tr 𝑦)}
39	38	eqabri 2894	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} ↔ (𝑤 ⊆ 𝑦 ∧ Tr 𝑦))
40	39	simprbi 500	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} → Tr 𝑦)
41	34, 40	mprg 3072	. . . . . . . . . . . 12 ⊢ Tr ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}
42	41	rgenw 3070	. . . . . . . . . . 11 ⊢ ∀𝑤 ∈ 𝑧 Tr ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}
43		triun 5212	. . . . . . . . . . 11 ⊢ (∀𝑤 ∈ 𝑧 Tr ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} → Tr ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)})
44	42, 43	ax-mp 5	. . . . . . . . . 10 ⊢ Tr ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}
45		df-tr 5198	. . . . . . . . . 10 ⊢ (Tr ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} ↔ ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} ⊆ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)})
46	44, 45	mpbi 232	. . . . . . . . 9 ⊢ ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} ⊆ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}
47		ssun4 4124	. . . . . . . . 9 ⊢ (∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} ⊆ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} → ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} ⊆ (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}))
48	46, 47	ax-mp 5	. . . . . . . 8 ⊢ ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} ⊆ (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)})
49	33, 48	unssi 4134	. . . . . . 7 ⊢ (∪ 𝑧 ∪ ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) ⊆ (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)})
50	25, 49	eqsstri 3973	. . . . . 6 ⊢ ∪ (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) ⊆ (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)})
51		df-tr 5198	. . . . . 6 ⊢ (Tr (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) ↔ ∪ (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) ⊆ (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}))
52	50, 51	mpbir 233	. . . . 5 ⊢ Tr (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)})
53		ssel 3921	. . . . . . . . . . . 12 ⊢ (𝑧 ⊆ 𝑦 → (𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦))
54		trss 5207	. . . . . . . . . . . 12 ⊢ (Tr 𝑦 → (𝑤 ∈ 𝑦 → 𝑤 ⊆ 𝑦))
55	53, 54	sylan9 514	. . . . . . . . . . 11 ⊢ ((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → (𝑤 ∈ 𝑧 → 𝑤 ⊆ 𝑦))
56		simpr 487	. . . . . . . . . . 11 ⊢ ((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → Tr 𝑦)
57	55, 56	jctird 533	. . . . . . . . . 10 ⊢ ((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → (𝑤 ∈ 𝑧 → (𝑤 ⊆ 𝑦 ∧ Tr 𝑦)))
58		rabab 3474	. . . . . . . . . . . 12 ⊢ {𝑥 ∈ V ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} = {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}
59	58	inteqi 4899	. . . . . . . . . . 11 ⊢ ∩ {𝑥 ∈ V ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} = ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}
60		vex 3448	. . . . . . . . . . . 12 ⊢ 𝑦 ∈ V
61	37	intminss 4922	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ V ∧ (𝑤 ⊆ 𝑦 ∧ Tr 𝑦)) → ∩ {𝑥 ∈ V ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} ⊆ 𝑦)
62	60, 61	mpan 698	. . . . . . . . . . 11 ⊢ ((𝑤 ⊆ 𝑦 ∧ Tr 𝑦) → ∩ {𝑥 ∈ V ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} ⊆ 𝑦)
63	59, 62	eqsstrrid 3966	. . . . . . . . . 10 ⊢ ((𝑤 ⊆ 𝑦 ∧ Tr 𝑦) → ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} ⊆ 𝑦)
64	57, 63	syl6 35	. . . . . . . . 9 ⊢ ((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → (𝑤 ∈ 𝑧 → ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} ⊆ 𝑦))
65	64	ralrimiv 3143	. . . . . . . 8 ⊢ ((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → ∀𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} ⊆ 𝑦)
66		iunss 4992	. . . . . . . 8 ⊢ (∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} ⊆ 𝑦 ↔ ∀𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} ⊆ 𝑦)
67	65, 66	sylibr 236	. . . . . . 7 ⊢ ((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} ⊆ 𝑦)
68		unss 4133	. . . . . . . 8 ⊢ ((𝑧 ⊆ 𝑦 ∧ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} ⊆ 𝑦) ↔ (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) ⊆ 𝑦)
69	68	biimpi 218	. . . . . . 7 ⊢ ((𝑧 ⊆ 𝑦 ∧ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} ⊆ 𝑦) → (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) ⊆ 𝑦)
70	67, 69	syldan 599	. . . . . 6 ⊢ ((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) ⊆ 𝑦)
71	70	ax-gen 1805	. . . . 5 ⊢ ∀𝑦((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) ⊆ 𝑦)
72	24, 52, 71	3pm3.2i 1349	. . . 4 ⊢ (𝑧 ⊆ (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) ∧ Tr (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) ∧ ∀𝑦((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) ⊆ 𝑦))
73		sseq2 3953	. . . . . . 7 ⊢ (𝑢 = (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) → (𝑧 ⊆ 𝑢 ↔ 𝑧 ⊆ (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)})))
74		treq 5204	. . . . . . 7 ⊢ (𝑢 = (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) → (Tr 𝑢 ↔ Tr (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)})))
75		sseq1 3952	. . . . . . . . 9 ⊢ (𝑢 = (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) → (𝑢 ⊆ 𝑦 ↔ (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) ⊆ 𝑦))
76	75	imbi2d 342	. . . . . . . 8 ⊢ (𝑢 = (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) → (((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑢 ⊆ 𝑦) ↔ ((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) ⊆ 𝑦)))
77	76	albidv 1930	. . . . . . 7 ⊢ (𝑢 = (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) → (∀𝑦((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑢 ⊆ 𝑦) ↔ ∀𝑦((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) ⊆ 𝑦)))
78	73, 74, 77	3anbi123d 1447	. . . . . 6 ⊢ (𝑢 = (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) → ((𝑧 ⊆ 𝑢 ∧ Tr 𝑢 ∧ ∀𝑦((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑢 ⊆ 𝑦)) ↔ (𝑧 ⊆ (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) ∧ Tr (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) ∧ ∀𝑦((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) ⊆ 𝑦))))
79	78	spcegv 3547	. . . . 5 ⊢ ((𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) ∈ V → ((𝑧 ⊆ (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) ∧ Tr (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) ∧ ∀𝑦((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) ⊆ 𝑦)) → ∃𝑢(𝑧 ⊆ 𝑢 ∧ Tr 𝑢 ∧ ∀𝑦((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑢 ⊆ 𝑦))))
80		sseq2 3953	. . . . . . 7 ⊢ (𝑢 = 𝑥 → (𝑧 ⊆ 𝑢 ↔ 𝑧 ⊆ 𝑥))
81		treq 5204	. . . . . . 7 ⊢ (𝑢 = 𝑥 → (Tr 𝑢 ↔ Tr 𝑥))
82		sseq1 3952	. . . . . . . . 9 ⊢ (𝑢 = 𝑥 → (𝑢 ⊆ 𝑦 ↔ 𝑥 ⊆ 𝑦))
83	82	imbi2d 342	. . . . . . . 8 ⊢ (𝑢 = 𝑥 → (((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑢 ⊆ 𝑦) ↔ ((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦)))
84	83	albidv 1930	. . . . . . 7 ⊢ (𝑢 = 𝑥 → (∀𝑦((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑢 ⊆ 𝑦) ↔ ∀𝑦((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦)))
85	80, 81, 84	3anbi123d 1447	. . . . . 6 ⊢ (𝑢 = 𝑥 → ((𝑧 ⊆ 𝑢 ∧ Tr 𝑢 ∧ ∀𝑦((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑢 ⊆ 𝑦)) ↔ (𝑧 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀𝑦((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦))))
86	85	cbvexvw 2047	. . . . 5 ⊢ (∃𝑢(𝑧 ⊆ 𝑢 ∧ Tr 𝑢 ∧ ∀𝑦((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑢 ⊆ 𝑦)) ↔ ∃𝑥(𝑧 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀𝑦((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦)))
87	79, 86	imbitrdi 253	. . . 4 ⊢ ((𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) ∈ V → ((𝑧 ⊆ (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) ∧ Tr (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) ∧ ∀𝑦((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) ⊆ 𝑦)) → ∃𝑥(𝑧 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀𝑦((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦))))
88	23, 72, 87	mpisyl 21	. . 3 ⊢ (∀𝑤 ∈ 𝑧 ∃𝑥(𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀𝑦((𝑤 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦)) → ∃𝑥(𝑧 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀𝑦((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦)))
89	13, 88	setinds2regs 35372	. 2 ⊢ ∃𝑥(𝑧 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀𝑦((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦))
90	1, 7, 89	vtocl 3515	1 ⊢ ∃𝑥(𝐴 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀𝑦((𝐴 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦))

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1095  ∀wal 1548   = wceq 1550  ∃wex 1789   ∈ wcel 2132  {cab 2730  ∀wral 3066  {crab 3404  Vcvv 3444   ∪ cun 3893   ⊆ wss 3895  ∪ cuni 4855  ∩ cint 4895  ∪ ciun 4939  Tr wtr 5197

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-8 2134  ax-9 2142  ax-10 2165  ax-11 2181  ax-12 2202  ax-ext 2724  ax-rep 5217  ax-sep 5236  ax-pr 5380  ax-un 7703  ax-regs 35367

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-3an 1097  df-tru 1553  df-fal 1563  df-ex 1790  df-nf 1794  df-sb 2081  df-mo 2556  df-clab 2731  df-cleq 2744  df-clel 2827  df-nfc 2901  df-ne 2948  df-ral 3067  df-rex 3077  df-rab 3405  df-v 3446  df-dif 3898  df-un 3900  df-in 3902  df-ss 3912  df-nul 4277  df-sn 4573  df-pr 4575  df-uni 4856  df-int 4896  df-iun 4941  df-iin 4942  df-tr 5198

This theorem is referenced by: (None)