Theorem tz9.1regs 35513

Description: Every set has a transitive closure (the smallest transitive extension). This version of tz9.1 9697 depends on ax-regs 35505 instead of ax-reg 9553 and ax-inf2 9609. This suggests a possible answer to the third question posed in tz9.1 9697, 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 9553 applies to them directly, but in a finitist context it seems that an axiom like ax-regs 35505 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 9628 using ax-reg 9553 and ax-inf2 9609 and as noinfepregs 35512 using ax-regs 35505. 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 35504. (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 3961	. . . 4 ⊢ (𝑧 = 𝐴 → (𝑧 ⊆ 𝑥 ↔ 𝐴 ⊆ 𝑥))
3		cleq1lem 15018	. . . . . 6 ⊢ (𝑧 = 𝐴 → ((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) ↔ (𝐴 ⊆ 𝑦 ∧ Tr 𝑦)))
4	3	imbi1d 344	. . . . 5 ⊢ (𝑧 = 𝐴 → (((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦) ↔ ((𝐴 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦)))
5	4	albidv 1948	. . . 4 ⊢ (𝑧 = 𝐴 → (∀𝑦((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦) ↔ ∀𝑦((𝐴 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦)))
6	2, 5	3anbi13d 1464	. . 3 ⊢ (𝑧 = 𝐴 → ((𝑧 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀𝑦((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦)) ↔ (𝐴 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀𝑦((𝐴 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦))))
7	6	exbidv 1949	. 2 ⊢ (𝑧 = 𝐴 → (∃𝑥(𝑧 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀𝑦((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦)) ↔ ∃𝑥(𝐴 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀𝑦((𝐴 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦))))
8		sseq1 3961	. . . . 5 ⊢ (𝑧 = 𝑤 → (𝑧 ⊆ 𝑥 ↔ 𝑤 ⊆ 𝑥))
9		cleq1lem 15018	. . . . . . 7 ⊢ (𝑧 = 𝑤 → ((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) ↔ (𝑤 ⊆ 𝑦 ∧ Tr 𝑦)))
10	9	imbi1d 344	. . . . . 6 ⊢ (𝑧 = 𝑤 → (((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦) ↔ ((𝑤 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦)))
11	10	albidv 1948	. . . . 5 ⊢ (𝑧 = 𝑤 → (∀𝑦((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦) ↔ ∀𝑦((𝑤 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦)))
12	8, 11	3anbi13d 1464	. . . 4 ⊢ (𝑧 = 𝑤 → ((𝑧 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀𝑦((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦)) ↔ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀𝑦((𝑤 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦))))
13	12	exbidv 1949	. . 3 ⊢ (𝑧 = 𝑤 → (∃𝑥(𝑧 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀𝑦((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦)) ↔ ∃𝑥(𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀𝑦((𝑤 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦))))
14		vex 3457	. . . . 5 ⊢ 𝑧 ∈ V
15		3simpa 1164	. . . . . . . . 9 ⊢ ((𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀𝑦((𝑤 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦)) → (𝑤 ⊆ 𝑥 ∧ Tr 𝑥))
16	15	eximi 1863	. . . . . . . 8 ⊢ (∃𝑥(𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀𝑦((𝑤 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦)) → ∃𝑥(𝑤 ⊆ 𝑥 ∧ Tr 𝑥))
17		intexab 5316	. . . . . . . 8 ⊢ (∃𝑥(𝑤 ⊆ 𝑥 ∧ Tr 𝑥) ↔ ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} ∈ V)
18	16, 17	sylib 221	. . . . . . 7 ⊢ (∃𝑥(𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀𝑦((𝑤 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦)) → ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} ∈ V)
19	18	ralimi 3100	. . . . . 6 ⊢ (∀𝑤 ∈ 𝑧 ∃𝑥(𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀𝑦((𝑤 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦)) → ∀𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} ∈ V)
20		iunexg 7959	. . . . . 6 ⊢ ((𝑧 ∈ V ∧ ∀𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} ∈ V) → ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} ∈ V)
21	14, 19, 20	sylancr 598	. . . . 5 ⊢ (∀𝑤 ∈ 𝑧 ∃𝑥(𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀𝑦((𝑤 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦)) → ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} ∈ V)
22		unexg 7741	. . . . 5 ⊢ ((𝑧 ∈ V ∧ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} ∈ V) → (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) ∈ V)
23	14, 21, 22	sylancr 598	. . . 4 ⊢ (∀𝑤 ∈ 𝑧 ∃𝑥(𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀𝑦((𝑤 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦)) → (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) ∈ V)
24		ssun1 4130	. . . . 5 ⊢ 𝑧 ⊆ (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)})
25		uniun 4894	. . . . . . 7 ⊢ ∪ (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) = (∪ 𝑧 ∪ ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)})
26		uniiun 5022	. . . . . . . . . 10 ⊢ ∪ 𝑧 = ∪ 𝑤 ∈ 𝑧 𝑤
27		ssmin 4931	. . . . . . . . . . . 12 ⊢ 𝑤 ⊆ ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}
28	27	rgenw 3081	. . . . . . . . . . 11 ⊢ ∀𝑤 ∈ 𝑧 𝑤 ⊆ ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}
29		ss2iun 4974	. . . . . . . . . . 11 ⊢ (∀𝑤 ∈ 𝑧 𝑤 ⊆ ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} → ∪ 𝑤 ∈ 𝑧 𝑤 ⊆ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)})
30	28, 29	ax-mp 5	. . . . . . . . . 10 ⊢ ∪ 𝑤 ∈ 𝑧 𝑤 ⊆ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}
31	26, 30	eqsstri 3982	. . . . . . . . 9 ⊢ ∪ 𝑧 ⊆ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}
32		ssun4 4133	. . . . . . . . 9 ⊢ (∪ 𝑧 ⊆ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} → ∪ 𝑧 ⊆ (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}))
33	31, 32	ax-mp 5	. . . . . . . 8 ⊢ ∪ 𝑧 ⊆ (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)})
34		trint 5235	. . . . . . . . . . . . 13 ⊢ (∀𝑦 ∈ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}Tr 𝑦 → Tr ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)})
35		sseq2 3962	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑦 → (𝑤 ⊆ 𝑥 ↔ 𝑤 ⊆ 𝑦))
36		treq 5224	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑦 → (Tr 𝑥 ↔ Tr 𝑦))
37	35, 36	anbi12d 643	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑦 → ((𝑤 ⊆ 𝑥 ∧ Tr 𝑥) ↔ (𝑤 ⊆ 𝑦 ∧ Tr 𝑦)))
38	37	cbvabv 2831	. . . . . . . . . . . . . . 15 ⊢ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} = {𝑦 ∣ (𝑤 ⊆ 𝑦 ∧ Tr 𝑦)}
39	38	eqabri 2903	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} ↔ (𝑤 ⊆ 𝑦 ∧ Tr 𝑦))
40	39	simprbi 502	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} → Tr 𝑦)
41	34, 40	mprg 3083	. . . . . . . . . . . 12 ⊢ Tr ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}
42	41	rgenw 3081	. . . . . . . . . . 11 ⊢ ∀𝑤 ∈ 𝑧 Tr ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}
43		triun 5232	. . . . . . . . . . 11 ⊢ (∀𝑤 ∈ 𝑧 Tr ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} → Tr ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)})
44	42, 43	ax-mp 5	. . . . . . . . . 10 ⊢ Tr ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}
45		df-tr 5218	. . . . . . . . . 10 ⊢ (Tr ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} ↔ ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} ⊆ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)})
46	44, 45	mpbi 233	. . . . . . . . 9 ⊢ ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} ⊆ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}
47		ssun4 4133	. . . . . . . . 9 ⊢ (∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} ⊆ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} → ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} ⊆ (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}))
48	46, 47	ax-mp 5	. . . . . . . 8 ⊢ ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} ⊆ (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)})
49	33, 48	unssi 4143	. . . . . . 7 ⊢ (∪ 𝑧 ∪ ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) ⊆ (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)})
50	25, 49	eqsstri 3982	. . . . . 6 ⊢ ∪ (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) ⊆ (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)})
51		df-tr 5218	. . . . . 6 ⊢ (Tr (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) ↔ ∪ (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) ⊆ (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}))
52	50, 51	mpbir 234	. . . . 5 ⊢ Tr (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)})
53		ssel 3930	. . . . . . . . . . . 12 ⊢ (𝑧 ⊆ 𝑦 → (𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦))
54		trss 5227	. . . . . . . . . . . 12 ⊢ (Tr 𝑦 → (𝑤 ∈ 𝑦 → 𝑤 ⊆ 𝑦))
55	53, 54	sylan9 516	. . . . . . . . . . 11 ⊢ ((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → (𝑤 ∈ 𝑧 → 𝑤 ⊆ 𝑦))
56		simpr 489	. . . . . . . . . . 11 ⊢ ((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → Tr 𝑦)
57	55, 56	jctird 535	. . . . . . . . . 10 ⊢ ((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → (𝑤 ∈ 𝑧 → (𝑤 ⊆ 𝑦 ∧ Tr 𝑦)))
58		rabab 3483	. . . . . . . . . . . 12 ⊢ {𝑥 ∈ V ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} = {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}
59	58	inteqi 4915	. . . . . . . . . . 11 ⊢ ∩ {𝑥 ∈ V ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} = ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}
60		vex 3457	. . . . . . . . . . . 12 ⊢ 𝑦 ∈ V
61	37	intminss 4938	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ V ∧ (𝑤 ⊆ 𝑦 ∧ Tr 𝑦)) → ∩ {𝑥 ∈ V ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} ⊆ 𝑦)
62	60, 61	mpan 702	. . . . . . . . . . 11 ⊢ ((𝑤 ⊆ 𝑦 ∧ Tr 𝑦) → ∩ {𝑥 ∈ V ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} ⊆ 𝑦)
63	59, 62	eqsstrrid 3975	. . . . . . . . . 10 ⊢ ((𝑤 ⊆ 𝑦 ∧ Tr 𝑦) → ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} ⊆ 𝑦)
64	57, 63	syl6 36	. . . . . . . . 9 ⊢ ((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → (𝑤 ∈ 𝑧 → ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} ⊆ 𝑦))
65	64	ralrimiv 3154	. . . . . . . 8 ⊢ ((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → ∀𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} ⊆ 𝑦)
66		iunss 5008	. . . . . . . 8 ⊢ (∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} ⊆ 𝑦 ↔ ∀𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} ⊆ 𝑦)
67	65, 66	sylibr 237	. . . . . . 7 ⊢ ((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} ⊆ 𝑦)
68		unss 4142	. . . . . . . 8 ⊢ ((𝑧 ⊆ 𝑦 ∧ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} ⊆ 𝑦) ↔ (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) ⊆ 𝑦)
69	68	biimpi 219	. . . . . . 7 ⊢ ((𝑧 ⊆ 𝑦 ∧ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} ⊆ 𝑦) → (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) ⊆ 𝑦)
70	67, 69	syldan 602	. . . . . 6 ⊢ ((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) ⊆ 𝑦)
71	70	ax-gen 1823	. . . . 5 ⊢ ∀𝑦((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) ⊆ 𝑦)
72	24, 52, 71	3pm3.2i 1356	. . . 4 ⊢ (𝑧 ⊆ (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) ∧ Tr (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) ∧ ∀𝑦((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) ⊆ 𝑦))
73		sseq2 3962	. . . . . . 7 ⊢ (𝑢 = (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) → (𝑧 ⊆ 𝑢 ↔ 𝑧 ⊆ (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)})))
74		treq 5224	. . . . . . 7 ⊢ (𝑢 = (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) → (Tr 𝑢 ↔ Tr (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)})))
75		sseq1 3961	. . . . . . . . 9 ⊢ (𝑢 = (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) → (𝑢 ⊆ 𝑦 ↔ (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) ⊆ 𝑦))
76	75	imbi2d 343	. . . . . . . 8 ⊢ (𝑢 = (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) → (((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑢 ⊆ 𝑦) ↔ ((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) ⊆ 𝑦)))
77	76	albidv 1948	. . . . . . 7 ⊢ (𝑢 = (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) → (∀𝑦((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑢 ⊆ 𝑦) ↔ ∀𝑦((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) ⊆ 𝑦)))
78	73, 74, 77	3anbi123d 1462	. . . . . 6 ⊢ (𝑢 = (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) → ((𝑧 ⊆ 𝑢 ∧ Tr 𝑢 ∧ ∀𝑦((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑢 ⊆ 𝑦)) ↔ (𝑧 ⊆ (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) ∧ Tr (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) ∧ ∀𝑦((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) ⊆ 𝑦))))
79	78	spcegv 3555	. . . . 5 ⊢ ((𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) ∈ V → ((𝑧 ⊆ (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) ∧ Tr (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) ∧ ∀𝑦((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) ⊆ 𝑦)) → ∃𝑢(𝑧 ⊆ 𝑢 ∧ Tr 𝑢 ∧ ∀𝑦((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑢 ⊆ 𝑦))))
80		sseq2 3962	. . . . . . 7 ⊢ (𝑢 = 𝑥 → (𝑧 ⊆ 𝑢 ↔ 𝑧 ⊆ 𝑥))
81		treq 5224	. . . . . . 7 ⊢ (𝑢 = 𝑥 → (Tr 𝑢 ↔ Tr 𝑥))
82		sseq1 3961	. . . . . . . . 9 ⊢ (𝑢 = 𝑥 → (𝑢 ⊆ 𝑦 ↔ 𝑥 ⊆ 𝑦))
83	82	imbi2d 343	. . . . . . . 8 ⊢ (𝑢 = 𝑥 → (((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑢 ⊆ 𝑦) ↔ ((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦)))
84	83	albidv 1948	. . . . . . 7 ⊢ (𝑢 = 𝑥 → (∀𝑦((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑢 ⊆ 𝑦) ↔ ∀𝑦((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦)))
85	80, 81, 84	3anbi123d 1462	. . . . . 6 ⊢ (𝑢 = 𝑥 → ((𝑧 ⊆ 𝑢 ∧ Tr 𝑢 ∧ ∀𝑦((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑢 ⊆ 𝑦)) ↔ (𝑧 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀𝑦((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦))))
86	85	cbvexvw 2065	. . . . 5 ⊢ (∃𝑢(𝑧 ⊆ 𝑢 ∧ Tr 𝑢 ∧ ∀𝑦((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑢 ⊆ 𝑦)) ↔ ∃𝑥(𝑧 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀𝑦((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦)))
87	79, 86	imbitrdi 254	. . . 4 ⊢ ((𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) ∈ V → ((𝑧 ⊆ (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) ∧ Tr (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) ∧ ∀𝑦((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) ⊆ 𝑦)) → ∃𝑥(𝑧 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀𝑦((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦))))
88	23, 72, 87	mpisyl 22	. . 3 ⊢ (∀𝑤 ∈ 𝑧 ∃𝑥(𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀𝑦((𝑤 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦)) → ∃𝑥(𝑧 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀𝑦((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦)))
89	13, 88	setinds2regs 35510	. 2 ⊢ ∃𝑥(𝑧 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀𝑦((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦))
90	1, 7, 89	vtocl 3524	1 ⊢ ∃𝑥(𝐴 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀𝑦((𝐴 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦))

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101  ∀wal 1566   = wceq 1568  ∃wex 1807   ∈ wcel 2141  {cab 2739  ∀wral 3077  {crab 3414  Vcvv 3453   ∪ cun 3902   ⊆ wss 3904  ∪ cuni 4871  ∩ cint 4911  ∪ ciun 4955  Tr wtr 5217

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-rep 5237  ax-sep 5256  ax-pr 5404  ax-un 7732  ax-regs 35505

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1571  df-fal 1581  df-ex 1808  df-nf 1812  df-sb 2095  df-mo 2565  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3415  df-v 3455  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-sn 4589  df-pr 4591  df-uni 4872  df-int 4912  df-iun 4957  df-iin 4958  df-tr 5218

This theorem is referenced by: (None)