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

Metamath Proof Explorer

Theorem opeliunxp

Description: Membership in a union of Cartesian products. (Contributed by Mario Carneiro, 29-Dec-2014) (Revised by Mario Carneiro, 1-Jan-2017)

Ref Expression
Assertion opeliunxp ( ⟨ 𝑥 , 𝐶 ⟩ ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝐶 ∈ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 df-iun ⊢ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ ( { 𝑥 } × 𝐵 ) }
2 1 eleq2i ⊢ ( ⟨ 𝑥 , 𝐶 ⟩ ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ↔ ⟨ 𝑥 , 𝐶 ⟩ ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ ( { 𝑥 } × 𝐵 ) } )
3 opex ⊢ ⟨ 𝑥 , 𝐶 ⟩ ∈ V
4 df-rex ⊢ ( ∃ 𝑥 ∈ 𝐴 𝑦 ∈ ( { 𝑥 } × 𝐵 ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( { 𝑥 } × 𝐵 ) ) )
5 nfv ⊢ Ⅎ 𝑧 ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( { 𝑥 } × 𝐵 ) )
6 nfs1v ⊢ Ⅎ 𝑥 [ 𝑧 / 𝑥 ] 𝑥 ∈ 𝐴
7 nfcv ⊢ Ⅎ 𝑥 { 𝑧 }
8 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑧 / 𝑥 ⦌ 𝐵
9 7 8 nfxp ⊢ Ⅎ 𝑥 ( { 𝑧 } × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 )
10 9 nfcri ⊢ Ⅎ 𝑥 𝑦 ∈ ( { 𝑧 } × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 )
11 6 10 nfan ⊢ Ⅎ 𝑥 ( [ 𝑧 / 𝑥 ] 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( { 𝑧 } × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) )
12 sbequ12 ⊢ ( 𝑥 = 𝑧 → ( 𝑥 ∈ 𝐴 ↔ [ 𝑧 / 𝑥 ] 𝑥 ∈ 𝐴 ) )
13 sneq ⊢ ( 𝑥 = 𝑧 → { 𝑥 } = { 𝑧 } )
14 csbeq1a ⊢ ( 𝑥 = 𝑧 → 𝐵 = ⦋ 𝑧 / 𝑥 ⦌ 𝐵 )
15 13 14 xpeq12d ⊢ ( 𝑥 = 𝑧 → ( { 𝑥 } × 𝐵 ) = ( { 𝑧 } × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) )
16 15 eleq2d ⊢ ( 𝑥 = 𝑧 → ( 𝑦 ∈ ( { 𝑥 } × 𝐵 ) ↔ 𝑦 ∈ ( { 𝑧 } × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ) )
17 12 16 anbi12d ⊢ ( 𝑥 = 𝑧 → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( { 𝑥 } × 𝐵 ) ) ↔ ( [ 𝑧 / 𝑥 ] 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( { 𝑧 } × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ) ) )
18 5 11 17 cbvexv1 ⊢ ( ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( { 𝑥 } × 𝐵 ) ) ↔ ∃ 𝑧 ( [ 𝑧 / 𝑥 ] 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( { 𝑧 } × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ) )
19 4 18 bitri ⊢ ( ∃ 𝑥 ∈ 𝐴 𝑦 ∈ ( { 𝑥 } × 𝐵 ) ↔ ∃ 𝑧 ( [ 𝑧 / 𝑥 ] 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( { 𝑧 } × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ) )
20 eleq1 ⊢ ( 𝑦 = ⟨ 𝑥 , 𝐶 ⟩ → ( 𝑦 ∈ ( { 𝑧 } × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ↔ ⟨ 𝑥 , 𝐶 ⟩ ∈ ( { 𝑧 } × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ) )
21 20 anbi2d ⊢ ( 𝑦 = ⟨ 𝑥 , 𝐶 ⟩ → ( ( [ 𝑧 / 𝑥 ] 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( { 𝑧 } × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ) ↔ ( [ 𝑧 / 𝑥 ] 𝑥 ∈ 𝐴 ∧ ⟨ 𝑥 , 𝐶 ⟩ ∈ ( { 𝑧 } × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ) ) )
22 21 exbidv ⊢ ( 𝑦 = ⟨ 𝑥 , 𝐶 ⟩ → ( ∃ 𝑧 ( [ 𝑧 / 𝑥 ] 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ ( { 𝑧 } × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ) ↔ ∃ 𝑧 ( [ 𝑧 / 𝑥 ] 𝑥 ∈ 𝐴 ∧ ⟨ 𝑥 , 𝐶 ⟩ ∈ ( { 𝑧 } × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ) ) )
23 19 22 bitrid ⊢ ( 𝑦 = ⟨ 𝑥 , 𝐶 ⟩ → ( ∃ 𝑥 ∈ 𝐴 𝑦 ∈ ( { 𝑥 } × 𝐵 ) ↔ ∃ 𝑧 ( [ 𝑧 / 𝑥 ] 𝑥 ∈ 𝐴 ∧ ⟨ 𝑥 , 𝐶 ⟩ ∈ ( { 𝑧 } × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ) ) )
24 3 23 elab ⊢ ( ⟨ 𝑥 , 𝐶 ⟩ ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ ( { 𝑥 } × 𝐵 ) } ↔ ∃ 𝑧 ( [ 𝑧 / 𝑥 ] 𝑥 ∈ 𝐴 ∧ ⟨ 𝑥 , 𝐶 ⟩ ∈ ( { 𝑧 } × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ) )
25 opelxp ⊢ ( ⟨ 𝑥 , 𝐶 ⟩ ∈ ( { 𝑧 } × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ↔ ( 𝑥 ∈ { 𝑧 } ∧ 𝐶 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) )
26 25 anbi2i ⊢ ( ( [ 𝑧 / 𝑥 ] 𝑥 ∈ 𝐴 ∧ ⟨ 𝑥 , 𝐶 ⟩ ∈ ( { 𝑧 } × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ) ↔ ( [ 𝑧 / 𝑥 ] 𝑥 ∈ 𝐴 ∧ ( 𝑥 ∈ { 𝑧 } ∧ 𝐶 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ) )
27 an12 ⊢ ( ( [ 𝑧 / 𝑥 ] 𝑥 ∈ 𝐴 ∧ ( 𝑥 ∈ { 𝑧 } ∧ 𝐶 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ) ↔ ( 𝑥 ∈ { 𝑧 } ∧ ( [ 𝑧 / 𝑥 ] 𝑥 ∈ 𝐴 ∧ 𝐶 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ) )
28 velsn ⊢ ( 𝑥 ∈ { 𝑧 } ↔ 𝑥 = 𝑧 )
29 equcom ⊢ ( 𝑥 = 𝑧 ↔ 𝑧 = 𝑥 )
30 28 29 bitri ⊢ ( 𝑥 ∈ { 𝑧 } ↔ 𝑧 = 𝑥 )
31 30 anbi1i ⊢ ( ( 𝑥 ∈ { 𝑧 } ∧ ( [ 𝑧 / 𝑥 ] 𝑥 ∈ 𝐴 ∧ 𝐶 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ) ↔ ( 𝑧 = 𝑥 ∧ ( [ 𝑧 / 𝑥 ] 𝑥 ∈ 𝐴 ∧ 𝐶 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ) )
32 26 27 31 3bitri ⊢ ( ( [ 𝑧 / 𝑥 ] 𝑥 ∈ 𝐴 ∧ ⟨ 𝑥 , 𝐶 ⟩ ∈ ( { 𝑧 } × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ) ↔ ( 𝑧 = 𝑥 ∧ ( [ 𝑧 / 𝑥 ] 𝑥 ∈ 𝐴 ∧ 𝐶 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ) )
33 32 exbii ⊢ ( ∃ 𝑧 ( [ 𝑧 / 𝑥 ] 𝑥 ∈ 𝐴 ∧ ⟨ 𝑥 , 𝐶 ⟩ ∈ ( { 𝑧 } × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ) ↔ ∃ 𝑧 ( 𝑧 = 𝑥 ∧ ( [ 𝑧 / 𝑥 ] 𝑥 ∈ 𝐴 ∧ 𝐶 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ) )
34 sbequ12r ⊢ ( 𝑧 = 𝑥 → ( [ 𝑧 / 𝑥 ] 𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐴 ) )
35 14 equcoms ⊢ ( 𝑧 = 𝑥 → 𝐵 = ⦋ 𝑧 / 𝑥 ⦌ 𝐵 )
36 35 eqcomd ⊢ ( 𝑧 = 𝑥 → ⦋ 𝑧 / 𝑥 ⦌ 𝐵 = 𝐵 )
37 36 eleq2d ⊢ ( 𝑧 = 𝑥 → ( 𝐶 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ↔ 𝐶 ∈ 𝐵 ) )
38 34 37 anbi12d ⊢ ( 𝑧 = 𝑥 → ( ( [ 𝑧 / 𝑥 ] 𝑥 ∈ 𝐴 ∧ 𝐶 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝐶 ∈ 𝐵 ) ) )
39 38 equsexvw ⊢ ( ∃ 𝑧 ( 𝑧 = 𝑥 ∧ ( [ 𝑧 / 𝑥 ] 𝑥 ∈ 𝐴 ∧ 𝐶 ∈ ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝐶 ∈ 𝐵 ) )
40 33 39 bitri ⊢ ( ∃ 𝑧 ( [ 𝑧 / 𝑥 ] 𝑥 ∈ 𝐴 ∧ ⟨ 𝑥 , 𝐶 ⟩ ∈ ( { 𝑧 } × ⦋ 𝑧 / 𝑥 ⦌ 𝐵 ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝐶 ∈ 𝐵 ) )
41 2 24 40 3bitri ⊢ ( ⟨ 𝑥 , 𝐶 ⟩ ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝐶 ∈ 𝐵 ) )