Metamath Proof Explorer

Theorem bnd2

Description: A variant of the Boundedness Axiom bnd that picks a subset z out of a possibly proper class B in which a property is true. (Contributed by NM, 4-Feb-2004)

Ref Expression
Hypothesis bnd2.1 ⊢ A ∈ V
Assertion bnd2 ⊢ ∀ x ∈ A ∃ y ∈ B φ → ∃ z z ⊆ B ∧ ∀ x ∈ A ∃ y ∈ z φ

Proof

Step Hyp Ref Expression
1 bnd2.1 ⊢ A ∈ V
2 df-rex ⊢ ∃ y ∈ B φ ↔ ∃ y y ∈ B ∧ φ
3 2 ralbii ⊢ ∀ x ∈ A ∃ y ∈ B φ ↔ ∀ x ∈ A ∃ y y ∈ B ∧ φ
4 raleq ⊢ v = A → ∀ x ∈ v ∃ y y ∈ B ∧ φ ↔ ∀ x ∈ A ∃ y y ∈ B ∧ φ
5 raleq ⊢ v = A → ∀ x ∈ v ∃ y ∈ w y ∈ B ∧ φ ↔ ∀ x ∈ A ∃ y ∈ w y ∈ B ∧ φ
6 5 exbidv ⊢ v = A → ∃ w ∀ x ∈ v ∃ y ∈ w y ∈ B ∧ φ ↔ ∃ w ∀ x ∈ A ∃ y ∈ w y ∈ B ∧ φ
7 4 6 imbi12d ⊢ v = A → ∀ x ∈ v ∃ y y ∈ B ∧ φ → ∃ w ∀ x ∈ v ∃ y ∈ w y ∈ B ∧ φ ↔ ∀ x ∈ A ∃ y y ∈ B ∧ φ → ∃ w ∀ x ∈ A ∃ y ∈ w y ∈ B ∧ φ
8 bnd ⊢ ∀ x ∈ v ∃ y y ∈ B ∧ φ → ∃ w ∀ x ∈ v ∃ y ∈ w y ∈ B ∧ φ
9 1 7 8 vtocl ⊢ ∀ x ∈ A ∃ y y ∈ B ∧ φ → ∃ w ∀ x ∈ A ∃ y ∈ w y ∈ B ∧ φ
10 3 9 sylbi ⊢ ∀ x ∈ A ∃ y ∈ B φ → ∃ w ∀ x ∈ A ∃ y ∈ w y ∈ B ∧ φ
11 vex ⊢ w ∈ V
12 11 inex1 ⊢ w ∩ B ∈ V
13 inss2 ⊢ w ∩ B ⊆ B
14 sseq1 ⊢ z = w ∩ B → z ⊆ B ↔ w ∩ B ⊆ B
15 13 14 mpbiri ⊢ z = w ∩ B → z ⊆ B
16 15 biantrurd ⊢ z = w ∩ B → ∀ x ∈ A ∃ y ∈ z φ ↔ z ⊆ B ∧ ∀ x ∈ A ∃ y ∈ z φ
17 rexeq ⊢ z = w ∩ B → ∃ y ∈ z φ ↔ ∃ y ∈ w ∩ B φ
18 rexin ⊢ ∃ y ∈ w ∩ B φ ↔ ∃ y ∈ w y ∈ B ∧ φ
19 17 18 bitrdi ⊢ z = w ∩ B → ∃ y ∈ z φ ↔ ∃ y ∈ w y ∈ B ∧ φ
20 19 ralbidv ⊢ z = w ∩ B → ∀ x ∈ A ∃ y ∈ z φ ↔ ∀ x ∈ A ∃ y ∈ w y ∈ B ∧ φ
21 16 20 bitr3d ⊢ z = w ∩ B → z ⊆ B ∧ ∀ x ∈ A ∃ y ∈ z φ ↔ ∀ x ∈ A ∃ y ∈ w y ∈ B ∧ φ
22 12 21 spcev ⊢ ∀ x ∈ A ∃ y ∈ w y ∈ B ∧ φ → ∃ z z ⊆ B ∧ ∀ x ∈ A ∃ y ∈ z φ
23 22 exlimiv ⊢ ∃ w ∀ x ∈ A ∃ y ∈ w y ∈ B ∧ φ → ∃ z z ⊆ B ∧ ∀ x ∈ A ∃ y ∈ z φ
24 10 23 syl ⊢ ∀ x ∈ A ∃ y ∈ B φ → ∃ z z ⊆ B ∧ ∀ x ∈ A ∃ y ∈ z φ