Axiom ax-sscoll 16683

Description: Axiom scheme of subset collection. It is stated with all possible disjoint variable conditions, to show that this weak form is sufficient. The antecedent means that 𝜑 represents a multivalued function from 𝑎 to 𝑏, or equivalently a collection of nonempty subsets of 𝑏 indexed by 𝑎, and the consequent asserts the existence of a subset of 𝑐 which "collects" at least one element in the image of each 𝑥 ∈ 𝑎 and which is made only of such elements. The axiom asserts the existence, for any sets 𝑎, 𝑏, of a set 𝑐 such that that implication holds for any value of the parameter 𝑧 of 𝜑. (Contributed by BJ, 5-Oct-2019.)

Assertion

Ref	Expression
ax-sscoll	⊢ ∀𝑎∀𝑏∃𝑐∀𝑧(∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝜑 → ∃𝑑 ∈ 𝑐 (∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑑 𝜑 ∧ ∀𝑦 ∈ 𝑑 ∃𝑥 ∈ 𝑎 𝜑))

Distinct variable groups:   𝑎,𝑏,𝑐,𝑑,𝑥,𝑦,𝑧   𝜑,𝑎,𝑏,𝑐,𝑑

Allowed substitution hints:   𝜑(𝑥,𝑦,𝑧)

Detailed syntax breakdown of Axiom ax-sscoll

Step	Hyp	Ref	Expression
1		wph	. . . . . . . 8 wff 𝜑
2		vy	. . . . . . . 8 setvar 𝑦
3		vb	. . . . . . . . 9 setvar 𝑏
4	3	cv 1397	. . . . . . . 8 class 𝑏
5	1, 2, 4	wrex 2512	. . . . . . 7 wff ∃𝑦 ∈ 𝑏 𝜑
6		vx	. . . . . . 7 setvar 𝑥
7		va	. . . . . . . 8 setvar 𝑎
8	7	cv 1397	. . . . . . 7 class 𝑎
9	5, 6, 8	wral 2511	. . . . . 6 wff ∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝜑
10		vd	. . . . . . . . . . 11 setvar 𝑑
11	10	cv 1397	. . . . . . . . . 10 class 𝑑
12	1, 2, 11	wrex 2512	. . . . . . . . 9 wff ∃𝑦 ∈ 𝑑 𝜑
13	12, 6, 8	wral 2511	. . . . . . . 8 wff ∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑑 𝜑
14	1, 6, 8	wrex 2512	. . . . . . . . 9 wff ∃𝑥 ∈ 𝑎 𝜑
15	14, 2, 11	wral 2511	. . . . . . . 8 wff ∀𝑦 ∈ 𝑑 ∃𝑥 ∈ 𝑎 𝜑
16	13, 15	wa 104	. . . . . . 7 wff (∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑑 𝜑 ∧ ∀𝑦 ∈ 𝑑 ∃𝑥 ∈ 𝑎 𝜑)
17		vc	. . . . . . . 8 setvar 𝑐
18	17	cv 1397	. . . . . . 7 class 𝑐
19	16, 10, 18	wrex 2512	. . . . . 6 wff ∃𝑑 ∈ 𝑐 (∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑑 𝜑 ∧ ∀𝑦 ∈ 𝑑 ∃𝑥 ∈ 𝑎 𝜑)
20	9, 19	wi 4	. . . . 5 wff (∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝜑 → ∃𝑑 ∈ 𝑐 (∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑑 𝜑 ∧ ∀𝑦 ∈ 𝑑 ∃𝑥 ∈ 𝑎 𝜑))
21		vz	. . . . 5 setvar 𝑧
22	20, 21	wal 1396	. . . 4 wff ∀𝑧(∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝜑 → ∃𝑑 ∈ 𝑐 (∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑑 𝜑 ∧ ∀𝑦 ∈ 𝑑 ∃𝑥 ∈ 𝑎 𝜑))
23	22, 17	wex 1541	. . 3 wff ∃𝑐∀𝑧(∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝜑 → ∃𝑑 ∈ 𝑐 (∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑑 𝜑 ∧ ∀𝑦 ∈ 𝑑 ∃𝑥 ∈ 𝑎 𝜑))
24	23, 3	wal 1396	. 2 wff ∀𝑏∃𝑐∀𝑧(∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝜑 → ∃𝑑 ∈ 𝑐 (∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑑 𝜑 ∧ ∀𝑦 ∈ 𝑑 ∃𝑥 ∈ 𝑎 𝜑))
25	24, 7	wal 1396	1 wff ∀𝑎∀𝑏∃𝑐∀𝑧(∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝜑 → ∃𝑑 ∈ 𝑐 (∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑑 𝜑 ∧ ∀𝑦 ∈ 𝑑 ∃𝑥 ∈ 𝑎 𝜑))

This axiom is referenced by:  sscoll2  16684