Description: A cartesian product of proper-class many sets is empty, because any function in the cartesian product has to be a set with domain A , which is not possible for a proper class domain. (Contributed by Mario Carneiro, 25-Jan-2015)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | ixpprc | ⊢ ( ¬ 𝐴 ∈ V → X 𝑥 ∈ 𝐴 𝐵 = ∅ ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | neq0 | ⊢ ( ¬ X 𝑥 ∈ 𝐴 𝐵 = ∅ ↔ ∃ 𝑓 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 ) | |
| 2 | ixpfn | ⊢ ( 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 → 𝑓 Fn 𝐴 ) | |
| 3 | fndm | ⊢ ( 𝑓 Fn 𝐴 → dom 𝑓 = 𝐴 ) | |
| 4 | vex | ⊢ 𝑓 ∈ V | |
| 5 | 4 | dmex | ⊢ dom 𝑓 ∈ V |
| 6 | 3 5 | eqeltrrdi | ⊢ ( 𝑓 Fn 𝐴 → 𝐴 ∈ V ) |
| 7 | 2 6 | syl | ⊢ ( 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 → 𝐴 ∈ V ) |
| 8 | 7 | exlimiv | ⊢ ( ∃ 𝑓 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 → 𝐴 ∈ V ) |
| 9 | 1 8 | sylbi | ⊢ ( ¬ X 𝑥 ∈ 𝐴 𝐵 = ∅ → 𝐴 ∈ V ) |
| 10 | 9 | con1i | ⊢ ( ¬ 𝐴 ∈ V → X 𝑥 ∈ 𝐴 𝐵 = ∅ ) |