Metamath Proof Explorer

Theorem eliunxp2

Description: Membership in a union of Cartesian products over its second component, analogous to eliunxp . (Contributed by AV, 30-Mar-2019)

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

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 excom ⊢ ( ∃ 𝑦 ∃ 𝑥 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ↔ ∃ 𝑥 ∃ 𝑦 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ )
8 6 7 sylibr ⊢ ( 𝐶 ∈ ∪ 𝑦 ∈ 𝐵 ( 𝐴 × { 𝑦 } ) → ∃ 𝑦 ∃ 𝑥 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ )
9 8 pm4.71ri ⊢ ( 𝐶 ∈ ∪ 𝑦 ∈ 𝐵 ( 𝐴 × { 𝑦 } ) ↔ ( ∃ 𝑦 ∃ 𝑥 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝐶 ∈ ∪ 𝑦 ∈ 𝐵 ( 𝐴 × { 𝑦 } ) ) )
10 nfiu1 ⊢ Ⅎ 𝑦 ∪ 𝑦 ∈ 𝐵 ( 𝐴 × { 𝑦 } )
11 10 nfel2 ⊢ Ⅎ 𝑦 𝐶 ∈ ∪ 𝑦 ∈ 𝐵 ( 𝐴 × { 𝑦 } )
12 11 19.41 ⊢ ( ∃ 𝑦 ( ∃ 𝑥 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝐶 ∈ ∪ 𝑦 ∈ 𝐵 ( 𝐴 × { 𝑦 } ) ) ↔ ( ∃ 𝑦 ∃ 𝑥 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝐶 ∈ ∪ 𝑦 ∈ 𝐵 ( 𝐴 × { 𝑦 } ) ) )
13 19.41v ⊢ ( ∃ 𝑥 ( 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝐶 ∈ ∪ 𝑦 ∈ 𝐵 ( 𝐴 × { 𝑦 } ) ) ↔ ( ∃ 𝑥 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝐶 ∈ ∪ 𝑦 ∈ 𝐵 ( 𝐴 × { 𝑦 } ) ) )
14 eleq1 ⊢ ( 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝐶 ∈ ∪ 𝑦 ∈ 𝐵 ( 𝐴 × { 𝑦 } ) ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ∪ 𝑦 ∈ 𝐵 ( 𝐴 × { 𝑦 } ) ) )
15 opeliun2xp ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ∪ 𝑦 ∈ 𝐵 ( 𝐴 × { 𝑦 } ) ↔ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐴 ) )
16 15 biancomi ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ∪ 𝑦 ∈ 𝐵 ( 𝐴 × { 𝑦 } ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) )
17 14 16 bitrdi ⊢ ( 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝐶 ∈ ∪ 𝑦 ∈ 𝐵 ( 𝐴 × { 𝑦 } ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) )
18 17 pm5.32i ⊢ ( ( 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝐶 ∈ ∪ 𝑦 ∈ 𝐵 ( 𝐴 × { 𝑦 } ) ) ↔ ( 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) )
19 18 exbii ⊢ ( ∃ 𝑥 ( 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝐶 ∈ ∪ 𝑦 ∈ 𝐵 ( 𝐴 × { 𝑦 } ) ) ↔ ∃ 𝑥 ( 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) )
20 13 19 bitr3i ⊢ ( ( ∃ 𝑥 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝐶 ∈ ∪ 𝑦 ∈ 𝐵 ( 𝐴 × { 𝑦 } ) ) ↔ ∃ 𝑥 ( 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) )
21 20 exbii ⊢ ( ∃ 𝑦 ( ∃ 𝑥 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝐶 ∈ ∪ 𝑦 ∈ 𝐵 ( 𝐴 × { 𝑦 } ) ) ↔ ∃ 𝑦 ∃ 𝑥 ( 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) )
22 9 12 21 3bitr2i ⊢ ( 𝐶 ∈ ∪ 𝑦 ∈ 𝐵 ( 𝐴 × { 𝑦 } ) ↔ ∃ 𝑦 ∃ 𝑥 ( 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) )
23 excom ⊢ ( ∃ 𝑦 ∃ 𝑥 ( 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) ↔ ∃ 𝑥 ∃ 𝑦 ( 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) )
24 22 23 bitri ⊢ ( 𝐶 ∈ ∪ 𝑦 ∈ 𝐵 ( 𝐴 × { 𝑦 } ) ↔ ∃ 𝑥 ∃ 𝑦 ( 𝐶 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) )