Theorem tz9.1regs 35102

Description: Every set has a transitive closure (the smallest transitive extension). This version of tz9.1 9614 depends on ax-regs 35096 instead of ax-reg 9473 and ax-inf2 9526. This suggests a possible answer to the third question posed in tz9.1 9614, 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 9473 applies to them directly, but in a finitist context it seems that an axiom like ax-regs 35096 is required since countably infinite classes are proper classes. (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 3958	. . . 4 ⊢ (𝑧 = 𝐴 → (𝑧 ⊆ 𝑥 ↔ 𝐴 ⊆ 𝑥))
3		cleq1lem 14881	. . . . . 6 ⊢ (𝑧 = 𝐴 → ((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) ↔ (𝐴 ⊆ 𝑦 ∧ Tr 𝑦)))
4	3	imbi1d 341	. . . . 5 ⊢ (𝑧 = 𝐴 → (((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦) ↔ ((𝐴 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦)))
5	4	albidv 1921	. . . 4 ⊢ (𝑧 = 𝐴 → (∀𝑦((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦) ↔ ∀𝑦((𝐴 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦)))
6	2, 5	3anbi13d 1440	. . 3 ⊢ (𝑧 = 𝐴 → ((𝑧 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀𝑦((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦)) ↔ (𝐴 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀𝑦((𝐴 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦))))
7	6	exbidv 1922	. 2 ⊢ (𝑧 = 𝐴 → (∃𝑥(𝑧 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀𝑦((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦)) ↔ ∃𝑥(𝐴 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀𝑦((𝐴 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦))))
8		sseq1 3958	. . . . 5 ⊢ (𝑧 = 𝑤 → (𝑧 ⊆ 𝑥 ↔ 𝑤 ⊆ 𝑥))
9		cleq1lem 14881	. . . . . . 7 ⊢ (𝑧 = 𝑤 → ((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) ↔ (𝑤 ⊆ 𝑦 ∧ Tr 𝑦)))
10	9	imbi1d 341	. . . . . 6 ⊢ (𝑧 = 𝑤 → (((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦) ↔ ((𝑤 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦)))
11	10	albidv 1921	. . . . 5 ⊢ (𝑧 = 𝑤 → (∀𝑦((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦) ↔ ∀𝑦((𝑤 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦)))
12	8, 11	3anbi13d 1440	. . . 4 ⊢ (𝑧 = 𝑤 → ((𝑧 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀𝑦((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦)) ↔ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀𝑦((𝑤 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦))))
13	12	exbidv 1922	. . 3 ⊢ (𝑧 = 𝑤 → (∃𝑥(𝑧 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀𝑦((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦)) ↔ ∃𝑥(𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀𝑦((𝑤 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦))))
14		vex 3438	. . . . 5 ⊢ 𝑧 ∈ V
15		3simpa 1148	. . . . . . . . 9 ⊢ ((𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀𝑦((𝑤 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦)) → (𝑤 ⊆ 𝑥 ∧ Tr 𝑥))
16	15	eximi 1836	. . . . . . . 8 ⊢ (∃𝑥(𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀𝑦((𝑤 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦)) → ∃𝑥(𝑤 ⊆ 𝑥 ∧ Tr 𝑥))
17		intexab 5282	. . . . . . . 8 ⊢ (∃𝑥(𝑤 ⊆ 𝑥 ∧ Tr 𝑥) ↔ ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} ∈ V)
18	16, 17	sylib 218	. . . . . . 7 ⊢ (∃𝑥(𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀𝑦((𝑤 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦)) → ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} ∈ V)
19	18	ralimi 3067	. . . . . 6 ⊢ (∀𝑤 ∈ 𝑧 ∃𝑥(𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀𝑦((𝑤 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦)) → ∀𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} ∈ V)
20		iunexg 7890	. . . . . 6 ⊢ ((𝑧 ∈ V ∧ ∀𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} ∈ V) → ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} ∈ V)
21	14, 19, 20	sylancr 587	. . . . 5 ⊢ (∀𝑤 ∈ 𝑧 ∃𝑥(𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀𝑦((𝑤 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦)) → ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} ∈ V)
22		unexg 7671	. . . . 5 ⊢ ((𝑧 ∈ V ∧ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} ∈ V) → (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) ∈ V)
23	14, 21, 22	sylancr 587	. . . 4 ⊢ (∀𝑤 ∈ 𝑧 ∃𝑥(𝑤 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀𝑦((𝑤 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦)) → (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) ∈ V)
24		ssun1 4126	. . . . 5 ⊢ 𝑧 ⊆ (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)})
25		uniun 4880	. . . . . . 7 ⊢ ∪ (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) = (∪ 𝑧 ∪ ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)})
26		uniiun 5005	. . . . . . . . . 10 ⊢ ∪ 𝑧 = ∪ 𝑤 ∈ 𝑧 𝑤
27		ssmin 4915	. . . . . . . . . . . 12 ⊢ 𝑤 ⊆ ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}
28	27	rgenw 3049	. . . . . . . . . . 11 ⊢ ∀𝑤 ∈ 𝑧 𝑤 ⊆ ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}
29		ss2iun 4958	. . . . . . . . . . 11 ⊢ (∀𝑤 ∈ 𝑧 𝑤 ⊆ ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} → ∪ 𝑤 ∈ 𝑧 𝑤 ⊆ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)})
30	28, 29	ax-mp 5	. . . . . . . . . 10 ⊢ ∪ 𝑤 ∈ 𝑧 𝑤 ⊆ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}
31	26, 30	eqsstri 3979	. . . . . . . . 9 ⊢ ∪ 𝑧 ⊆ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}
32		ssun4 4129	. . . . . . . . 9 ⊢ (∪ 𝑧 ⊆ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} → ∪ 𝑧 ⊆ (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}))
33	31, 32	ax-mp 5	. . . . . . . 8 ⊢ ∪ 𝑧 ⊆ (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)})
34		trint 5213	. . . . . . . . . . . . 13 ⊢ (∀𝑦 ∈ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}Tr 𝑦 → Tr ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)})
35		sseq2 3959	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑦 → (𝑤 ⊆ 𝑥 ↔ 𝑤 ⊆ 𝑦))
36		treq 5203	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑦 → (Tr 𝑥 ↔ Tr 𝑦))
37	35, 36	anbi12d 632	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑦 → ((𝑤 ⊆ 𝑥 ∧ Tr 𝑥) ↔ (𝑤 ⊆ 𝑦 ∧ Tr 𝑦)))
38	37	cbvabv 2800	. . . . . . . . . . . . . . 15 ⊢ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} = {𝑦 ∣ (𝑤 ⊆ 𝑦 ∧ Tr 𝑦)}
39	38	eqabri 2872	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} ↔ (𝑤 ⊆ 𝑦 ∧ Tr 𝑦))
40	39	simprbi 496	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} → Tr 𝑦)
41	34, 40	mprg 3051	. . . . . . . . . . . 12 ⊢ Tr ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}
42	41	rgenw 3049	. . . . . . . . . . 11 ⊢ ∀𝑤 ∈ 𝑧 Tr ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}
43		triun 5210	. . . . . . . . . . 11 ⊢ (∀𝑤 ∈ 𝑧 Tr ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} → Tr ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)})
44	42, 43	ax-mp 5	. . . . . . . . . 10 ⊢ Tr ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}
45		df-tr 5197	. . . . . . . . . 10 ⊢ (Tr ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} ↔ ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} ⊆ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)})
46	44, 45	mpbi 230	. . . . . . . . 9 ⊢ ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} ⊆ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}
47		ssun4 4129	. . . . . . . . 9 ⊢ (∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} ⊆ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} → ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} ⊆ (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}))
48	46, 47	ax-mp 5	. . . . . . . 8 ⊢ ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} ⊆ (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)})
49	33, 48	unssi 4139	. . . . . . 7 ⊢ (∪ 𝑧 ∪ ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) ⊆ (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)})
50	25, 49	eqsstri 3979	. . . . . 6 ⊢ ∪ (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) ⊆ (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)})
51		df-tr 5197	. . . . . 6 ⊢ (Tr (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) ↔ ∪ (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) ⊆ (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}))
52	50, 51	mpbir 231	. . . . 5 ⊢ Tr (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)})
53		ssel 3926	. . . . . . . . . . . 12 ⊢ (𝑧 ⊆ 𝑦 → (𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦))
54		trss 5206	. . . . . . . . . . . 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 3465	. . . . . . . . . . . 12 ⊢ {𝑥 ∈ V ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} = {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}
59	58	inteqi 4899	. . . . . . . . . . 11 ⊢ ∩ {𝑥 ∈ V ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} = ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}
60		vex 3438	. . . . . . . . . . . 12 ⊢ 𝑦 ∈ V
61	37	intminss 4922	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ V ∧ (𝑤 ⊆ 𝑦 ∧ Tr 𝑦)) → ∩ {𝑥 ∈ V ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} ⊆ 𝑦)
62	60, 61	mpan 690	. . . . . . . . . . 11 ⊢ ((𝑤 ⊆ 𝑦 ∧ Tr 𝑦) → ∩ {𝑥 ∈ V ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} ⊆ 𝑦)
63	59, 62	eqsstrrid 3972	. . . . . . . . . 10 ⊢ ((𝑤 ⊆ 𝑦 ∧ Tr 𝑦) → ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} ⊆ 𝑦)
64	57, 63	syl6 35	. . . . . . . . 9 ⊢ ((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → (𝑤 ∈ 𝑧 → ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} ⊆ 𝑦))
65	64	ralrimiv 3121	. . . . . . . 8 ⊢ ((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → ∀𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} ⊆ 𝑦)
66		iunss 4992	. . . . . . . 8 ⊢ (∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} ⊆ 𝑦 ↔ ∀𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} ⊆ 𝑦)
67	65, 66	sylibr 234	. . . . . . 7 ⊢ ((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} ⊆ 𝑦)
68		unss 4138	. . . . . . . 8 ⊢ ((𝑧 ⊆ 𝑦 ∧ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} ⊆ 𝑦) ↔ (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) ⊆ 𝑦)
69	68	biimpi 216	. . . . . . 7 ⊢ ((𝑧 ⊆ 𝑦 ∧ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)} ⊆ 𝑦) → (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) ⊆ 𝑦)
70	67, 69	syldan 591	. . . . . 6 ⊢ ((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) ⊆ 𝑦)
71	70	ax-gen 1796	. . . . 5 ⊢ ∀𝑦((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) ⊆ 𝑦)
72	24, 52, 71	3pm3.2i 1340	. . . 4 ⊢ (𝑧 ⊆ (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) ∧ Tr (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) ∧ ∀𝑦((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) ⊆ 𝑦))
73		sseq2 3959	. . . . . . 7 ⊢ (𝑢 = (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) → (𝑧 ⊆ 𝑢 ↔ 𝑧 ⊆ (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)})))
74		treq 5203	. . . . . . 7 ⊢ (𝑢 = (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) → (Tr 𝑢 ↔ Tr (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)})))
75		sseq1 3958	. . . . . . . . 9 ⊢ (𝑢 = (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) → (𝑢 ⊆ 𝑦 ↔ (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) ⊆ 𝑦))
76	75	imbi2d 340	. . . . . . . 8 ⊢ (𝑢 = (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) → (((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑢 ⊆ 𝑦) ↔ ((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) ⊆ 𝑦)))
77	76	albidv 1921	. . . . . . 7 ⊢ (𝑢 = (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) → (∀𝑦((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑢 ⊆ 𝑦) ↔ ∀𝑦((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) ⊆ 𝑦)))
78	73, 74, 77	3anbi123d 1438	. . . . . 6 ⊢ (𝑢 = (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) → ((𝑧 ⊆ 𝑢 ∧ Tr 𝑢 ∧ ∀𝑦((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑢 ⊆ 𝑦)) ↔ (𝑧 ⊆ (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) ∧ Tr (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) ∧ ∀𝑦((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) ⊆ 𝑦))))
79	78	spcegv 3550	. . . . 5 ⊢ ((𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) ∈ V → ((𝑧 ⊆ (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) ∧ Tr (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) ∧ ∀𝑦((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → (𝑧 ∪ ∪ 𝑤 ∈ 𝑧 ∩ {𝑥 ∣ (𝑤 ⊆ 𝑥 ∧ Tr 𝑥)}) ⊆ 𝑦)) → ∃𝑢(𝑧 ⊆ 𝑢 ∧ Tr 𝑢 ∧ ∀𝑦((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑢 ⊆ 𝑦))))
80		sseq2 3959	. . . . . . 7 ⊢ (𝑢 = 𝑥 → (𝑧 ⊆ 𝑢 ↔ 𝑧 ⊆ 𝑥))
81		treq 5203	. . . . . . 7 ⊢ (𝑢 = 𝑥 → (Tr 𝑢 ↔ Tr 𝑥))
82		sseq1 3958	. . . . . . . . 9 ⊢ (𝑢 = 𝑥 → (𝑢 ⊆ 𝑦 ↔ 𝑥 ⊆ 𝑦))
83	82	imbi2d 340	. . . . . . . 8 ⊢ (𝑢 = 𝑥 → (((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑢 ⊆ 𝑦) ↔ ((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦)))
84	83	albidv 1921	. . . . . . 7 ⊢ (𝑢 = 𝑥 → (∀𝑦((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑢 ⊆ 𝑦) ↔ ∀𝑦((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦)))
85	80, 81, 84	3anbi123d 1438	. . . . . 6 ⊢ (𝑢 = 𝑥 → ((𝑧 ⊆ 𝑢 ∧ Tr 𝑢 ∧ ∀𝑦((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑢 ⊆ 𝑦)) ↔ (𝑧 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀𝑦((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦))))
86	85	cbvexvw 2038	. . . . 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 35101	. 2 ⊢ ∃𝑥(𝑧 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀𝑦((𝑧 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦))
90	1, 7, 89	vtocl 3511	1 ⊢ ∃𝑥(𝐴 ⊆ 𝑥 ∧ Tr 𝑥 ∧ ∀𝑦((𝐴 ⊆ 𝑦 ∧ Tr 𝑦) → 𝑥 ⊆ 𝑦))

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086  ∀wal 1539   = wceq 1541  ∃wex 1780   ∈ wcel 2110  {cab 2708  ∀wral 3045  {crab 3393  Vcvv 3434   ∪ cun 3898   ⊆ wss 3900  ∪ cuni 4857  ∩ cint 4895  ∪ ciun 4939  Tr wtr 5196

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2112  ax-9 2120  ax-10 2143  ax-11 2159  ax-12 2179  ax-ext 2702  ax-rep 5215  ax-sep 5232  ax-nul 5242  ax-pr 5368  ax-un 7663  ax-regs 35096

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2534  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-ral 3046  df-rex 3055  df-rab 3394  df-v 3436  df-dif 3903  df-un 3905  df-in 3907  df-ss 3917  df-nul 4282  df-sn 4575  df-pr 4577  df-uni 4858  df-int 4896  df-iun 4941  df-iin 4942  df-tr 5197

This theorem is referenced by: (None)