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

Metamath Proof Explorer

Theorem eliunxp

Description: Membership in a union of Cartesian products. Analogue of elxp for nonconstant B ( x ) . (Contributed by Mario Carneiro, 29-Dec-2014)

Ref Expression
Assertion eliunxp ( 𝐶 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ↔ ∃ 𝑥 ∃ 𝑦 ( 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 relxp ⊢ Rel ( { 𝑥 } × 𝐵 )
2 1 rgenw ⊢ ∀ 𝑥 ∈ 𝐴 Rel ( { 𝑥 } × 𝐵 )
3 reliun ⊢ ( Rel ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ↔ ∀ 𝑥 ∈ 𝐴 Rel ( { 𝑥 } × 𝐵 ) )
4 2 3 mpbir ⊢ Rel ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 )
5 elrel ⊢ ( ( Rel ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ∧ 𝐶 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ) → ∃ 𝑥 ∃ 𝑦 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ )
6 4 5 mpan ⊢ ( 𝐶 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) → ∃ 𝑥 ∃ 𝑦 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ )
7 6 pm4.71ri ⊢ ( 𝐶 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ↔ ( ∃ 𝑥 ∃ 𝑦 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝐶 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ) )
8 nfiu1 ⊢ Ⅎ 𝑥 ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 )
9 8 nfel2 ⊢ Ⅎ 𝑥 𝐶 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 )
10 9 19.41 ⊢ ( ∃ 𝑥 ( ∃ 𝑦 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝐶 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ) ↔ ( ∃ 𝑥 ∃ 𝑦 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝐶 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ) )
11 19.41v ⊢ ( ∃ 𝑦 ( 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝐶 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ) ↔ ( ∃ 𝑦 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝐶 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ) )
12 eleq1 ⊢ ( 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝐶 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ) )
13 opeliunxp ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) )
14 12 13 bitrdi ⊢ ( 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝐶 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) )
15 14 pm5.32i ⊢ ( ( 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝐶 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ) ↔ ( 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) )
16 15 exbii ⊢ ( ∃ 𝑦 ( 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝐶 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ) ↔ ∃ 𝑦 ( 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) )
17 11 16 bitr3i ⊢ ( ( ∃ 𝑦 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝐶 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ) ↔ ∃ 𝑦 ( 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) )
18 17 exbii ⊢ ( ∃ 𝑥 ( ∃ 𝑦 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝐶 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ) ↔ ∃ 𝑥 ∃ 𝑦 ( 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) )
19 7 10 18 3bitr2i ⊢ ( 𝐶 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ↔ ∃ 𝑥 ∃ 𝑦 ( 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) )