Description: Existence of a set of functions. In contrast to fabex or fabexg , the condition in the class abstraction does not contain the function explicitly, but the function can be derived from it. Therefore, this theorem is also applicable for more special functions like one-to-one, onto or one-to-one onto functions. (Contributed by AV, 20-May-2025)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | fabexd.f | ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑓 : 𝑋 ⟶ 𝑌 ) | |
| fabexd.x | ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 ) | ||
| fabexd.y | ⊢ ( 𝜑 → 𝑌 ∈ 𝑊 ) | ||
| Assertion | fabexd | ⊢ ( 𝜑 → { 𝑓 ∣ 𝜓 } ∈ V ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | fabexd.f | ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑓 : 𝑋 ⟶ 𝑌 ) | |
| 2 | fabexd.x | ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 ) | |
| 3 | fabexd.y | ⊢ ( 𝜑 → 𝑌 ∈ 𝑊 ) | |
| 4 | 2 3 | xpexd | ⊢ ( 𝜑 → ( 𝑋 × 𝑌 ) ∈ V ) |
| 5 | 4 | pwexd | ⊢ ( 𝜑 → 𝒫 ( 𝑋 × 𝑌 ) ∈ V ) |
| 6 | fssxp | ⊢ ( 𝑓 : 𝑋 ⟶ 𝑌 → 𝑓 ⊆ ( 𝑋 × 𝑌 ) ) | |
| 7 | velpw | ⊢ ( 𝑓 ∈ 𝒫 ( 𝑋 × 𝑌 ) ↔ 𝑓 ⊆ ( 𝑋 × 𝑌 ) ) | |
| 8 | 6 7 | sylibr | ⊢ ( 𝑓 : 𝑋 ⟶ 𝑌 → 𝑓 ∈ 𝒫 ( 𝑋 × 𝑌 ) ) |
| 9 | 1 8 | syl | ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑓 ∈ 𝒫 ( 𝑋 × 𝑌 ) ) |
| 10 | 9 | ex | ⊢ ( 𝜑 → ( 𝜓 → 𝑓 ∈ 𝒫 ( 𝑋 × 𝑌 ) ) ) |
| 11 | 10 | abssdv | ⊢ ( 𝜑 → { 𝑓 ∣ 𝜓 } ⊆ 𝒫 ( 𝑋 × 𝑌 ) ) |
| 12 | 5 11 | ssexd | ⊢ ( 𝜑 → { 𝑓 ∣ 𝜓 } ∈ V ) |