Users' Mathboxes Mathbox for BJ < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >   Mathboxes  >  ax-sscoll GIF version

Axiom ax-sscoll 14742
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
StepHypRef Expression
1 wph . . . . . . . 8 wff 𝜑
2 vy . . . . . . . 8 setvar 𝑦
3 vb . . . . . . . . 9 setvar 𝑏
43cv 1352 . . . . . . . 8 class 𝑏
51, 2, 4wrex 2456 . . . . . . 7 wff 𝑦𝑏 𝜑
6 vx . . . . . . 7 setvar 𝑥
7 va . . . . . . . 8 setvar 𝑎
87cv 1352 . . . . . . 7 class 𝑎
95, 6, 8wral 2455 . . . . . 6 wff 𝑥𝑎𝑦𝑏 𝜑
10 vd . . . . . . . . . . 11 setvar 𝑑
1110cv 1352 . . . . . . . . . 10 class 𝑑
121, 2, 11wrex 2456 . . . . . . . . 9 wff 𝑦𝑑 𝜑
1312, 6, 8wral 2455 . . . . . . . 8 wff 𝑥𝑎𝑦𝑑 𝜑
141, 6, 8wrex 2456 . . . . . . . . 9 wff 𝑥𝑎 𝜑
1514, 2, 11wral 2455 . . . . . . . 8 wff 𝑦𝑑𝑥𝑎 𝜑
1613, 15wa 104 . . . . . . 7 wff (∀𝑥𝑎𝑦𝑑 𝜑 ∧ ∀𝑦𝑑𝑥𝑎 𝜑)
17 vc . . . . . . . 8 setvar 𝑐
1817cv 1352 . . . . . . 7 class 𝑐
1916, 10, 18wrex 2456 . . . . . 6 wff 𝑑𝑐 (∀𝑥𝑎𝑦𝑑 𝜑 ∧ ∀𝑦𝑑𝑥𝑎 𝜑)
209, 19wi 4 . . . . 5 wff (∀𝑥𝑎𝑦𝑏 𝜑 → ∃𝑑𝑐 (∀𝑥𝑎𝑦𝑑 𝜑 ∧ ∀𝑦𝑑𝑥𝑎 𝜑))
21 vz . . . . 5 setvar 𝑧
2220, 21wal 1351 . . . 4 wff 𝑧(∀𝑥𝑎𝑦𝑏 𝜑 → ∃𝑑𝑐 (∀𝑥𝑎𝑦𝑑 𝜑 ∧ ∀𝑦𝑑𝑥𝑎 𝜑))
2322, 17wex 1492 . . 3 wff 𝑐𝑧(∀𝑥𝑎𝑦𝑏 𝜑 → ∃𝑑𝑐 (∀𝑥𝑎𝑦𝑑 𝜑 ∧ ∀𝑦𝑑𝑥𝑎 𝜑))
2423, 3wal 1351 . 2 wff 𝑏𝑐𝑧(∀𝑥𝑎𝑦𝑏 𝜑 → ∃𝑑𝑐 (∀𝑥𝑎𝑦𝑑 𝜑 ∧ ∀𝑦𝑑𝑥𝑎 𝜑))
2524, 7wal 1351 1 wff 𝑎𝑏𝑐𝑧(∀𝑥𝑎𝑦𝑏 𝜑 → ∃𝑑𝑐 (∀𝑥𝑎𝑦𝑑 𝜑 ∧ ∀𝑦𝑑𝑥𝑎 𝜑))
Colors of variables: wff set class
This axiom is referenced by:  sscoll2  14743
  Copyright terms: Public domain W3C validator