Mathbox for BJ |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > Mathboxes > ax-strcoll | GIF version |
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 4081. (Contributed by BJ, 5-Oct-2019.) |
Ref | Expression |
---|---|
ax-strcoll | ⊢ ∀𝑎(∀𝑥 ∈ 𝑎 ∃𝑦𝜑 → ∃𝑏(∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝜑 ∧ ∀𝑦 ∈ 𝑏 ∃𝑥 ∈ 𝑎 𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wph | . . . . 5 wff 𝜑 | |
2 | vy | . . . . 5 setvar 𝑦 | |
3 | 1, 2 | wex 1472 | . . . 4 wff ∃𝑦𝜑 |
4 | vx | . . . 4 setvar 𝑥 | |
5 | va | . . . . 5 setvar 𝑎 | |
6 | 5 | cv 1334 | . . . 4 class 𝑎 |
7 | 3, 4, 6 | wral 2435 | . . 3 wff ∀𝑥 ∈ 𝑎 ∃𝑦𝜑 |
8 | vb | . . . . . . . 8 setvar 𝑏 | |
9 | 8 | cv 1334 | . . . . . . 7 class 𝑏 |
10 | 1, 2, 9 | wrex 2436 | . . . . . 6 wff ∃𝑦 ∈ 𝑏 𝜑 |
11 | 10, 4, 6 | wral 2435 | . . . . 5 wff ∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝜑 |
12 | 1, 4, 6 | wrex 2436 | . . . . . 6 wff ∃𝑥 ∈ 𝑎 𝜑 |
13 | 12, 2, 9 | wral 2435 | . . . . 5 wff ∀𝑦 ∈ 𝑏 ∃𝑥 ∈ 𝑎 𝜑 |
14 | 11, 13 | wa 103 | . . . 4 wff (∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝜑 ∧ ∀𝑦 ∈ 𝑏 ∃𝑥 ∈ 𝑎 𝜑) |
15 | 14, 8 | wex 1472 | . . 3 wff ∃𝑏(∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝜑 ∧ ∀𝑦 ∈ 𝑏 ∃𝑥 ∈ 𝑎 𝜑) |
16 | 7, 15 | wi 4 | . 2 wff (∀𝑥 ∈ 𝑎 ∃𝑦𝜑 → ∃𝑏(∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝜑 ∧ ∀𝑦 ∈ 𝑏 ∃𝑥 ∈ 𝑎 𝜑)) |
17 | 16, 5 | wal 1333 | 1 wff ∀𝑎(∀𝑥 ∈ 𝑎 ∃𝑦𝜑 → ∃𝑏(∀𝑥 ∈ 𝑎 ∃𝑦 ∈ 𝑏 𝜑 ∧ ∀𝑦 ∈ 𝑏 ∃𝑥 ∈ 𝑎 𝜑)) |
Colors of variables: wff set class |
This axiom is referenced by: strcoll2 13629 |
Copyright terms: Public domain | W3C validator |