Theorem tz9.1regs 35284

Description: Every set has a transitive closure (the smallest transitive extension). This version of tz9.1 9639 depends on ax-regs 35276 instead of ax-reg 9498 and ax-inf2 9551. This suggests a possible answer to the third question posed in tz9.1 9639, 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 9498 applies to them directly, but in a finitist context it seems that an axiom like ax-regs 35276 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 9570 using ax-reg 9498 and ax-inf2 9551 and as noinfepregs 35283 using ax-regs 35276. 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 35275. (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 3948	. . . 4 ⊢ (𝑧 = 𝐴 → (𝑧 ⊆ 𝑥 ↔ 𝐴 ⊆ 𝑥))
3		cleq1lem 14906	. . . . . 6 ⊢ (𝑧 = 𝐴 → ((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) ↔ (𝐴 ⊆ 𝑦 ∧ Tr 𝑦)))
4	3	imbi1d 341	. . . . 5 ⊢ (𝑧 = 𝐴 → (((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦) ↔ ((𝐴 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦)))
5	4	albidv 1922	. . . 4 ⊢ (𝑧 = 𝐴 → (∀𝑦((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦) ↔ ∀𝑦((𝐴 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦)))
6	2, 5	3anbi13d 1441	. . 3 ⊢ (𝑧 = 𝐴 → ((𝑧 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀𝑦((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦)) ↔ (𝐴 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀𝑦((𝐴 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦))))
7	6	exbidv 1923	. 2 ⊢ (𝑧 = 𝐴 → (∃𝑥(𝑧 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀𝑦((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦)) ↔ ∃𝑥(𝐴 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀𝑦((𝐴 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦))))
8		sseq1 3948	. . . . 5 ⊢ (𝑧 = 𝑤 → (𝑧 ⊆ 𝑥 ↔ 𝑤 ⊆ 𝑥))
9		cleq1lem 14906	. . . . . . 7 ⊢ (𝑧 = 𝑤 → ((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) ↔ (𝑤 ⊆ 𝑦 ∧ Tr 𝑦)))
10	9	imbi1d 341	. . . . . 6 ⊢ (𝑧 = 𝑤 → (((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦) ↔ ((𝑤 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦)))
11	10	albidv 1922	. . . . 5 ⊢ (𝑧 = 𝑤 → (∀𝑦((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦) ↔ ∀𝑦((𝑤 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦)))
12	8, 11	3anbi13d 1441	. . . 4 ⊢ (𝑧 = 𝑤 → ((𝑧 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀𝑦((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦)) ↔ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀𝑦((𝑤 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦))))
13	12	exbidv 1923	. . 3 ⊢ (𝑧 = 𝑤 → (∃𝑥(𝑧 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀𝑦((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦)) ↔ ∃𝑥(𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀𝑦((𝑤 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦))))
14		vex 3434	. . . . 5 ⊢ 𝑧 ∈ V
15		3simpa 1149	. . . . . . . . 9 ⊢ ((𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀𝑦((𝑤 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦)) → (𝑤 ⊆ 𝑥 ∧ Tr 𝑥))
16	15	eximi 1837	. . . . . . . 8 ⊢ (∃𝑥(𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀𝑦((𝑤 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦)) → ∃𝑥(𝑤 ⊆ 𝑥 ∧ Tr 𝑥))
17		intexab 5281	. . . . . . . 8 ⊢ (∃𝑥(𝑤 ⊆ 𝑥 ∧ Tr 𝑥) ↔ ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} ∈ V)
18	16, 17	sylib 218	. . . . . . 7 ⊢ (∃𝑥(𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀𝑦((𝑤 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦)) → ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} ∈ V)
19	18	ralimi 3075	. . . . . 6 ⊢ (∀𝑤 ∈ 𝑧 ∃𝑥(𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀𝑦((𝑤 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦)) → ∀𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} ∈ V)
20		iunexg 7907	. . . . . 6 ⊢ ((𝑧 ∈ V ∧ ∀𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} ∈ V) → ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} ∈ V)
21	14, 19, 20	sylancr 588	. . . . 5 ⊢ (∀𝑤 ∈ 𝑧 ∃𝑥(𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀𝑦((𝑤 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦)) → ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} ∈ V)
22		unexg 7688	. . . . 5 ⊢ ((𝑧 ∈ V ∧ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} ∈ V) → (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) ∈ V)
23	14, 21, 22	sylancr 588	. . . 4 ⊢ (∀𝑤 ∈ 𝑧 ∃𝑥(𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀𝑦((𝑤 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦)) → (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) ∈ V)
24		ssun1 4119	. . . . 5 ⊢ 𝑧 ⊆ (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)})
25		uniun 4874	. . . . . . 7 ⊢ ∪ (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) = (∪ 𝑧 ∪ ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)})
26		uniiun 5002	. . . . . . . . . 10 ⊢ ∪ 𝑧 = ∪ 𝑤 ∈ 𝑧 𝑤
27		ssmin 4910	. . . . . . . . . . . 12 ⊢ 𝑤 ⊆ ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}
28	27	rgenw 3056	. . . . . . . . . . 11 ⊢ ∀𝑤 ∈ 𝑧 𝑤 ⊆ ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}
29		ss2iun 4953	. . . . . . . . . . 11 ⊢ (∀𝑤 ∈ 𝑧 𝑤 ⊆ ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} → ∪ 𝑤 ∈ 𝑧 𝑤 ⊆ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)})
30	28, 29	ax-mp 5	. . . . . . . . . 10 ⊢ ∪ 𝑤 ∈ 𝑧 𝑤 ⊆ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}
31	26, 30	eqsstri 3969	. . . . . . . . 9 ⊢ ∪ 𝑧 ⊆ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}
32		ssun4 4122	. . . . . . . . 9 ⊢ (∪ 𝑧 ⊆ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} → ∪ 𝑧 ⊆ (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}))
33	31, 32	ax-mp 5	. . . . . . . 8 ⊢ ∪ 𝑧 ⊆ (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)})
34		trint 5210	. . . . . . . . . . . . 13 ⊢ (∀𝑦 ∈ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}Tr 𝑦 → Tr ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)})
35		sseq2 3949	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑦 → (𝑤 ⊆ 𝑥 ↔ 𝑤 ⊆ 𝑦))
36		treq 5200	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑦 → (Tr 𝑥 ↔ Tr 𝑦))
37	35, 36	anbi12d 633	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑦 → ((𝑤 ⊆ 𝑥 ∧ Tr 𝑥) ↔ (𝑤 ⊆ 𝑦 ∧ Tr 𝑦)))
38	37	cbvabv 2807	. . . . . . . . . . . . . . 15 ⊢ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} = {𝑦 ∣ (𝑤 ⊆ 𝑦 ∧ Tr 𝑦)}
39	38	eqabri 2879	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} ↔ (𝑤 ⊆ 𝑦 ∧ Tr 𝑦))
40	39	simprbi 497	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} → Tr 𝑦)
41	34, 40	mprg 3058	. . . . . . . . . . . 12 ⊢ Tr ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}
42	41	rgenw 3056	. . . . . . . . . . 11 ⊢ ∀𝑤 ∈ 𝑧 Tr ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}
43		triun 5207	. . . . . . . . . . 11 ⊢ (∀𝑤 ∈ 𝑧 Tr ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} → Tr ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)})
44	42, 43	ax-mp 5	. . . . . . . . . 10 ⊢ Tr ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}
45		df-tr 5194	. . . . . . . . . 10 ⊢ (Tr ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} ↔ ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} ⊆ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)})
46	44, 45	mpbi 230	. . . . . . . . 9 ⊢ ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} ⊆ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}
47		ssun4 4122	. . . . . . . . 9 ⊢ (∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} ⊆ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} → ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} ⊆ (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}))
48	46, 47	ax-mp 5	. . . . . . . 8 ⊢ ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} ⊆ (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)})
49	33, 48	unssi 4132	. . . . . . 7 ⊢ (∪ 𝑧 ∪ ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) ⊆ (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)})
50	25, 49	eqsstri 3969	. . . . . 6 ⊢ ∪ (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) ⊆ (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)})
51		df-tr 5194	. . . . . 6 ⊢ (Tr (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) ↔ ∪ (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) ⊆ (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}))
52	50, 51	mpbir 231	. . . . 5 ⊢ Tr (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)})
53		ssel 3916	. . . . . . . . . . . 12 ⊢ (𝑧 ⊆ 𝑦 → (𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦))
54		trss 5203	. . . . . . . . . . . 12 ⊢ (Tr 𝑦 → (𝑤 ∈ 𝑦 → 𝑤 ⊆ 𝑦))
55	53, 54	sylan9 507	. . . . . . . . . . 11 ⊢ ((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → (𝑤 ∈ 𝑧 → 𝑤 ⊆ 𝑦))
56		simpr 484	. . . . . . . . . . 11 ⊢ ((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → Tr 𝑦)
57	55, 56	jctird 526	. . . . . . . . . 10 ⊢ ((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → (𝑤 ∈ 𝑧 → (𝑤 ⊆ 𝑦 ∧ Tr 𝑦)))
58		rabab 3461	. . . . . . . . . . . 12 ⊢ {𝑥 ∈ V ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} = {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}
59	58	inteqi 4894	. . . . . . . . . . 11 ⊢ ∩ {𝑥 ∈ V ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} = ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}
60		vex 3434	. . . . . . . . . . . 12 ⊢ 𝑦 ∈ V
61	37	intminss 4917	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ V ∧ (𝑤 ⊆ 𝑦 ∧ Tr 𝑦)) → ∩ {𝑥 ∈ V ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} ⊆ 𝑦)
62	60, 61	mpan 691	. . . . . . . . . . 11 ⊢ ((𝑤 ⊆ 𝑦 ∧ Tr 𝑦) → ∩ {𝑥 ∈ V ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} ⊆ 𝑦)
63	59, 62	eqsstrrid 3962	. . . . . . . . . 10 ⊢ ((𝑤 ⊆ 𝑦 ∧ Tr 𝑦) → ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} ⊆ 𝑦)
64	57, 63	syl6 35	. . . . . . . . 9 ⊢ ((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → (𝑤 ∈ 𝑧 → ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} ⊆ 𝑦))
65	64	ralrimiv 3129	. . . . . . . 8 ⊢ ((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → ∀𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} ⊆ 𝑦)
66		iunss 4988	. . . . . . . 8 ⊢ (∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} ⊆ 𝑦 ↔ ∀𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} ⊆ 𝑦)
67	65, 66	sylibr 234	. . . . . . 7 ⊢ ((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} ⊆ 𝑦)
68		unss 4131	. . . . . . . 8 ⊢ ((𝑧 ⊆ 𝑦 ∧ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} ⊆ 𝑦) ↔ (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) ⊆ 𝑦)
69	68	biimpi 216	. . . . . . 7 ⊢ ((𝑧 ⊆ 𝑦 ∧ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} ⊆ 𝑦) → (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) ⊆ 𝑦)
70	67, 69	syldan 592	. . . . . 6 ⊢ ((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) ⊆ 𝑦)
71	70	ax-gen 1797	. . . . 5 ⊢ ∀𝑦((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) ⊆ 𝑦)
72	24, 52, 71	3pm3.2i 1341	. . . 4 ⊢ (𝑧 ⊆ (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) ∧ Tr (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) ∧ ∀𝑦((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) ⊆ 𝑦))
73		sseq2 3949	. . . . . . 7 ⊢ (𝑢 = (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) → (𝑧 ⊆ 𝑢 ↔ 𝑧 ⊆ (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)})))
74		treq 5200	. . . . . . 7 ⊢ (𝑢 = (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) → (Tr 𝑢 ↔ Tr (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)})))
75		sseq1 3948	. . . . . . . . 9 ⊢ (𝑢 = (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) → (𝑢 ⊆ 𝑦 ↔ (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) ⊆ 𝑦))
76	75	imbi2d 340	. . . . . . . 8 ⊢ (𝑢 = (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) → (((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑢 ⊆ 𝑦) ↔ ((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) ⊆ 𝑦)))
77	76	albidv 1922	. . . . . . 7 ⊢ (𝑢 = (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) → (∀𝑦((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑢 ⊆ 𝑦) ↔ ∀𝑦((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) ⊆ 𝑦)))
78	73, 74, 77	3anbi123d 1439	. . . . . 6 ⊢ (𝑢 = (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) → ((𝑧 ⊆ 𝑢 ∧ Tr 𝑢 ∧ ∀𝑦((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑢 ⊆ 𝑦)) ↔ (𝑧 ⊆ (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) ∧ Tr (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) ∧ ∀𝑦((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) ⊆ 𝑦))))
79	78	spcegv 3540	. . . . 5 ⊢ ((𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) ∈ V → ((𝑧 ⊆ (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) ∧ Tr (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) ∧ ∀𝑦((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) ⊆ 𝑦)) → ∃𝑢(𝑧 ⊆ 𝑢 ∧ Tr 𝑢 ∧ ∀𝑦((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑢 ⊆ 𝑦))))
80		sseq2 3949	. . . . . . 7 ⊢ (𝑢 = 𝑥 → (𝑧 ⊆ 𝑢 ↔ 𝑧 ⊆ 𝑥))
81		treq 5200	. . . . . . 7 ⊢ (𝑢 = 𝑥 → (Tr 𝑢 ↔ Tr 𝑥))
82		sseq1 3948	. . . . . . . . 9 ⊢ (𝑢 = 𝑥 → (𝑢 ⊆ 𝑦 ↔ 𝑥 ⊆ 𝑦))
83	82	imbi2d 340	. . . . . . . 8 ⊢ (𝑢 = 𝑥 → (((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑢 ⊆ 𝑦) ↔ ((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦)))
84	83	albidv 1922	. . . . . . 7 ⊢ (𝑢 = 𝑥 → (∀𝑦((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑢 ⊆ 𝑦) ↔ ∀𝑦((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦)))
85	80, 81, 84	3anbi123d 1439	. . . . . 6 ⊢ (𝑢 = 𝑥 → ((𝑧 ⊆ 𝑢 ∧ Tr 𝑢 ∧ ∀𝑦((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑢 ⊆ 𝑦)) ↔ (𝑧 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀𝑦((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦))))
86	85	cbvexvw 2039	. . . . 5 ⊢ (∃𝑢(𝑧 ⊆ 𝑢 ∧ Tr 𝑢 ∧ ∀𝑦((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑢 ⊆ 𝑦)) ↔ ∃𝑥(𝑧 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀𝑦((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦)))
87	79, 86	imbitrdi 251	. . . 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 35281	. 2 ⊢ ∃𝑥(𝑧 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀𝑦((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦))
90	1, 7, 89	vtocl 3504	1 ⊢ ∃𝑥(𝐴 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀𝑦((𝐴 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦))

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087  ∀wal 1540   = wceq 1542  ∃wex 1781   ∈ wcel 2114  {cab 2715  ∀wral 3052  {crab 3390  Vcvv 3430   ∪ cun 3888   ⊆ wss 3890  ∪ cuni 4851  ∩ cint 4890  ∪ ciun 4934  Tr wtr 5193

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-rep 5212  ax-sep 5231  ax-pr 5368  ax-un 7680  ax-regs 35276

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-sn 4569  df-pr 4571  df-uni 4852  df-int 4891  df-iun 4936  df-iin 4937  df-tr 5194

This theorem is referenced by: (None)