Metamath Proof Explorer

Theorem disjenex

Description: Existence version of disjen . (Contributed by Mario Carneiro, 7-Feb-2015)

Ref Expression
Assertion disjenex ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ∃ 𝑥 ( ( 𝐴 ∩ 𝑥 ) = ∅ ∧ 𝑥 ≈ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 simpr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → 𝐵 ∈ 𝑊 )
2 snex ⊢ { 𝒫 ∪ ran 𝐴 } ∈ V
3 xpexg ⊢ ( ( 𝐵 ∈ 𝑊 ∧ { 𝒫 ∪ ran 𝐴 } ∈ V ) → ( 𝐵 × { 𝒫 ∪ ran 𝐴 } ) ∈ V )
4 1 2 3 sylancl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐵 × { 𝒫 ∪ ran 𝐴 } ) ∈ V )
5 disjen ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( 𝐴 ∩ ( 𝐵 × { 𝒫 ∪ ran 𝐴 } ) ) = ∅ ∧ ( 𝐵 × { 𝒫 ∪ ran 𝐴 } ) ≈ 𝐵 ) )
6 ineq2 ⊢ ( 𝑥 = ( 𝐵 × { 𝒫 ∪ ran 𝐴 } ) → ( 𝐴 ∩ 𝑥 ) = ( 𝐴 ∩ ( 𝐵 × { 𝒫 ∪ ran 𝐴 } ) ) )
7 6 eqeq1d ⊢ ( 𝑥 = ( 𝐵 × { 𝒫 ∪ ran 𝐴 } ) → ( ( 𝐴 ∩ 𝑥 ) = ∅ ↔ ( 𝐴 ∩ ( 𝐵 × { 𝒫 ∪ ran 𝐴 } ) ) = ∅ ) )
8 breq1 ⊢ ( 𝑥 = ( 𝐵 × { 𝒫 ∪ ran 𝐴 } ) → ( 𝑥 ≈ 𝐵 ↔ ( 𝐵 × { 𝒫 ∪ ran 𝐴 } ) ≈ 𝐵 ) )
9 7 8 anbi12d ⊢ ( 𝑥 = ( 𝐵 × { 𝒫 ∪ ran 𝐴 } ) → ( ( ( 𝐴 ∩ 𝑥 ) = ∅ ∧ 𝑥 ≈ 𝐵 ) ↔ ( ( 𝐴 ∩ ( 𝐵 × { 𝒫 ∪ ran 𝐴 } ) ) = ∅ ∧ ( 𝐵 × { 𝒫 ∪ ran 𝐴 } ) ≈ 𝐵 ) ) )
10 4 5 9 spcedv ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ∃ 𝑥 ( ( 𝐴 ∩ 𝑥 ) = ∅ ∧ 𝑥 ≈ 𝐵 ) )