This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem xpexr

Description: If a Cartesian product is a set, one of its components must be a set. (Contributed by NM, 27-Aug-2006)

Ref Expression
Assertion xpexr ( ( 𝐴 × 𝐵 ) ∈ 𝐶 → ( 𝐴 ∈ V ∨ 𝐵 ∈ V ) )

Proof

Step Hyp Ref Expression
1 0ex ⊢ ∅ ∈ V
2 eleq1 ⊢ ( 𝐴 = ∅ → ( 𝐴 ∈ V ↔ ∅ ∈ V ) )
3 1 2 mpbiri ⊢ ( 𝐴 = ∅ → 𝐴 ∈ V )
4 3 pm2.24d ⊢ ( 𝐴 = ∅ → ( ¬ 𝐴 ∈ V → 𝐵 ∈ V ) )
5 4 a1d ⊢ ( 𝐴 = ∅ → ( ( 𝐴 × 𝐵 ) ∈ 𝐶 → ( ¬ 𝐴 ∈ V → 𝐵 ∈ V ) ) )
6 rnexg ⊢ ( ( 𝐴 × 𝐵 ) ∈ 𝐶 → ran ( 𝐴 × 𝐵 ) ∈ V )
7 rnxp ⊢ ( 𝐴 ≠ ∅ → ran ( 𝐴 × 𝐵 ) = 𝐵 )
8 7 eleq1d ⊢ ( 𝐴 ≠ ∅ → ( ran ( 𝐴 × 𝐵 ) ∈ V ↔ 𝐵 ∈ V ) )
9 6 8 imbitrid ⊢ ( 𝐴 ≠ ∅ → ( ( 𝐴 × 𝐵 ) ∈ 𝐶 → 𝐵 ∈ V ) )
10 9 a1dd ⊢ ( 𝐴 ≠ ∅ → ( ( 𝐴 × 𝐵 ) ∈ 𝐶 → ( ¬ 𝐴 ∈ V → 𝐵 ∈ V ) ) )
11 5 10 pm2.61ine ⊢ ( ( 𝐴 × 𝐵 ) ∈ 𝐶 → ( ¬ 𝐴 ∈ V → 𝐵 ∈ V ) )
12 11 orrd ⊢ ( ( 𝐴 × 𝐵 ) ∈ 𝐶 → ( 𝐴 ∈ V ∨ 𝐵 ∈ V ) )