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 ⊢ 𝐴 ∈ V
Assertion bnd2 ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 → ∃ 𝑧 ( 𝑧 ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝑧 𝜑 ) )

Proof

Step Hyp Ref Expression
1 bnd2.1 ⊢ 𝐴 ∈ V
2 df-rex ⊢ ( ∃ 𝑦 ∈ 𝐵 𝜑 ↔ ∃ 𝑦 ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) )
3 2 ralbii ⊢ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 ↔ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) )
4 raleq ⊢ ( 𝑣 = 𝐴 → ( ∀ 𝑥 ∈ 𝑣 ∃ 𝑦 ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ↔ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ) )
5 raleq ⊢ ( 𝑣 = 𝐴 → ( ∀ 𝑥 ∈ 𝑣 ∃ 𝑦 ∈ 𝑤 ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ↔ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝑤 ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ) )
6 5 exbidv ⊢ ( 𝑣 = 𝐴 → ( ∃ 𝑤 ∀ 𝑥 ∈ 𝑣 ∃ 𝑦 ∈ 𝑤 ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ↔ ∃ 𝑤 ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝑤 ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ) )
7 4 6 imbi12d ⊢ ( 𝑣 = 𝐴 → ( ( ∀ 𝑥 ∈ 𝑣 ∃ 𝑦 ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) → ∃ 𝑤 ∀ 𝑥 ∈ 𝑣 ∃ 𝑦 ∈ 𝑤 ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ) ↔ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) → ∃ 𝑤 ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝑤 ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ) ) )
8 bnd ⊢ ( ∀ 𝑥 ∈ 𝑣 ∃ 𝑦 ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) → ∃ 𝑤 ∀ 𝑥 ∈ 𝑣 ∃ 𝑦 ∈ 𝑤 ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) )
9 1 7 8 vtocl ⊢ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) → ∃ 𝑤 ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝑤 ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) )
10 3 9 sylbi ⊢ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 → ∃ 𝑤 ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝑤 ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) )
11 vex ⊢ 𝑤 ∈ V
12 11 inex1 ⊢ ( 𝑤 ∩ 𝐵 ) ∈ V
13 inss2 ⊢ ( 𝑤 ∩ 𝐵 ) ⊆ 𝐵
14 sseq1 ⊢ ( 𝑧 = ( 𝑤 ∩ 𝐵 ) → ( 𝑧 ⊆ 𝐵 ↔ ( 𝑤 ∩ 𝐵 ) ⊆ 𝐵 ) )
15 13 14 mpbiri ⊢ ( 𝑧 = ( 𝑤 ∩ 𝐵 ) → 𝑧 ⊆ 𝐵 )
16 15 biantrurd ⊢ ( 𝑧 = ( 𝑤 ∩ 𝐵 ) → ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝑧 𝜑 ↔ ( 𝑧 ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝑧 𝜑 ) ) )
17 rexeq ⊢ ( 𝑧 = ( 𝑤 ∩ 𝐵 ) → ( ∃ 𝑦 ∈ 𝑧 𝜑 ↔ ∃ 𝑦 ∈ ( 𝑤 ∩ 𝐵 ) 𝜑 ) )
18 rexin ⊢ ( ∃ 𝑦 ∈ ( 𝑤 ∩ 𝐵 ) 𝜑 ↔ ∃ 𝑦 ∈ 𝑤 ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) )
19 17 18 bitrdi ⊢ ( 𝑧 = ( 𝑤 ∩ 𝐵 ) → ( ∃ 𝑦 ∈ 𝑧 𝜑 ↔ ∃ 𝑦 ∈ 𝑤 ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ) )
20 19 ralbidv ⊢ ( 𝑧 = ( 𝑤 ∩ 𝐵 ) → ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝑧 𝜑 ↔ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝑤 ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ) )
21 16 20 bitr3d ⊢ ( 𝑧 = ( 𝑤 ∩ 𝐵 ) → ( ( 𝑧 ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝑧 𝜑 ) ↔ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝑤 ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) ) )
22 12 21 spcev ⊢ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝑤 ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) → ∃ 𝑧 ( 𝑧 ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝑧 𝜑 ) )
23 22 exlimiv ⊢ ( ∃ 𝑤 ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝑤 ( 𝑦 ∈ 𝐵 ∧ 𝜑 ) → ∃ 𝑧 ( 𝑧 ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝑧 𝜑 ) )
24 10 23 syl ⊢ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 → ∃ 𝑧 ( 𝑧 ⊆ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝑧 𝜑 ) )