Axiom ax-strcoll 14017

Description: Axiom scheme of strong 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 on 𝑎, or equivalently a collection of nonempty classes indexed by 𝑎, and the axiom asserts the existence of a set 𝑏 which "collects" at least one element in the image of each 𝑥 ∈ 𝑎 and which is made only of such elements. That second conjunct is what makes it "strong", compared to the axiom scheme of collection ax-coll 4104. (Contributed by BJ, 5-Oct-2019.)

Assertion

Ref	Expression
ax-strcoll	⊢ ∀𝑎(∀𝑥 ∈ 𝑎 ∃𝑦𝜑 → ∃𝑏(∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝜑 ∧ ∀𝑦 ∈ 𝑏 ∃𝑥 ∈ 𝑎 𝜑))

Distinct variable groups:   𝑎,𝑏,𝑥,𝑦   𝜑,𝑎,𝑏

Allowed substitution hints:   𝜑(𝑥,𝑦)

Detailed syntax breakdown of Axiom ax-strcoll

Step	Hyp	Ref	Expression
1		wph	. . . . 5 wff 𝜑
2		vy	. . . . 5 setvar 𝑦
3	1, 2	wex 1485	. . . 4 wff ∃𝑦𝜑
4		vx	. . . 4 setvar 𝑥
5		va	. . . . 5 setvar 𝑎
6	5	cv 1347	. . . 4 class 𝑎
7	3, 4, 6	wral 2448	. . 3 wff ∀𝑥 ∈ 𝑎 ∃𝑦𝜑
8		vb	. . . . . . . 8 setvar 𝑏
9	8	cv 1347	. . . . . . 7 class 𝑏
10	1, 2, 9	wrex 2449	. . . . . 6 wff ∃𝑦 ∈ 𝑏 𝜑
11	10, 4, 6	wral 2448	. . . . 5 wff ∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝜑
12	1, 4, 6	wrex 2449	. . . . . 6 wff ∃𝑥 ∈ 𝑎 𝜑
13	12, 2, 9	wral 2448	. . . . 5 wff ∀𝑦 ∈ 𝑏 ∃𝑥 ∈ 𝑎 𝜑
14	11, 13	wa 103	. . . 4 wff (∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝜑 ∧ ∀𝑦 ∈ 𝑏 ∃𝑥 ∈ 𝑎 𝜑)
15	14, 8	wex 1485	. . 3 wff ∃𝑏(∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝜑 ∧ ∀𝑦 ∈ 𝑏 ∃𝑥 ∈ 𝑎 𝜑)
16	7, 15	wi 4	. 2 wff (∀𝑥 ∈ 𝑎 ∃𝑦𝜑 → ∃𝑏(∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝜑 ∧ ∀𝑦 ∈ 𝑏 ∃𝑥 ∈ 𝑎 𝜑))
17	16, 5	wal 1346	1 wff ∀𝑎(∀𝑥 ∈ 𝑎 ∃𝑦𝜑 → ∃𝑏(∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝜑 ∧ ∀𝑦 ∈ 𝑏 ∃𝑥 ∈ 𝑎 𝜑))

This axiom is referenced by:  strcoll2  14018