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

Metamath Proof Explorer

Theorem opeliun2xp

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

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

Proof

Step Hyp Ref Expression
1 df-iun ⊢ ∪ 𝑦 ∈ 𝐵 ( 𝐴 × { 𝑦 } ) = { 𝑥 ∣ ∃ 𝑦 ∈ 𝐵 𝑥 ∈ ( 𝐴 × { 𝑦 } ) }
2 1 eleq2i ⊢ ( ⟨ 𝐶 , 𝑦 ⟩ ∈ ∪ 𝑦 ∈ 𝐵 ( 𝐴 × { 𝑦 } ) ↔ ⟨ 𝐶 , 𝑦 ⟩ ∈ { 𝑥 ∣ ∃ 𝑦 ∈ 𝐵 𝑥 ∈ ( 𝐴 × { 𝑦 } ) } )
3 opex ⊢ ⟨ 𝐶 , 𝑦 ⟩ ∈ V
4 df-rex ⊢ ( ∃ 𝑦 ∈ 𝐵 𝑥 ∈ ( 𝐴 × { 𝑦 } ) ↔ ∃ 𝑦 ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ ( 𝐴 × { 𝑦 } ) ) )
5 nfv ⊢ Ⅎ 𝑧 ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ ( 𝐴 × { 𝑦 } ) )
6 nfs1v ⊢ Ⅎ 𝑦 [ 𝑧 / 𝑦 ] 𝑦 ∈ 𝐵
7 nfcsb1v ⊢ Ⅎ 𝑦 ⦋ 𝑧 / 𝑦 ⦌ 𝐴
8 nfcv ⊢ Ⅎ 𝑦 { 𝑧 }
9 7 8 nfxp ⊢ Ⅎ 𝑦 ( ⦋ 𝑧 / 𝑦 ⦌ 𝐴 × { 𝑧 } )
10 9 nfcri ⊢ Ⅎ 𝑦 𝑥 ∈ ( ⦋ 𝑧 / 𝑦 ⦌ 𝐴 × { 𝑧 } )
11 6 10 nfan ⊢ Ⅎ 𝑦 ( [ 𝑧 / 𝑦 ] 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ ( ⦋ 𝑧 / 𝑦 ⦌ 𝐴 × { 𝑧 } ) )
12 sbequ12 ⊢ ( 𝑦 = 𝑧 → ( 𝑦 ∈ 𝐵 ↔ [ 𝑧 / 𝑦 ] 𝑦 ∈ 𝐵 ) )
13 csbeq1a ⊢ ( 𝑦 = 𝑧 → 𝐴 = ⦋ 𝑧 / 𝑦 ⦌ 𝐴 )
14 sneq ⊢ ( 𝑦 = 𝑧 → { 𝑦 } = { 𝑧 } )
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 an13 ⊢ ( ( [ 𝑧 / 𝑦 ] 𝑦 ∈ 𝐵 ∧ ( 𝐶 ∈ ⦋ 𝑧 / 𝑦 ⦌ 𝐴 ∧ 𝑦 ∈ { 𝑧 } ) ) ↔ ( 𝑦 ∈ { 𝑧 } ∧ ( 𝐶 ∈ ⦋ 𝑧 / 𝑦 ⦌ 𝐴 ∧ [ 𝑧 / 𝑦 ] 𝑦 ∈ 𝐵 ) ) )
28 ancom ⊢ ( ( 𝐶 ∈ ⦋ 𝑧 / 𝑦 ⦌ 𝐴 ∧ [ 𝑧 / 𝑦 ] 𝑦 ∈ 𝐵 ) ↔ ( [ 𝑧 / 𝑦 ] 𝑦 ∈ 𝐵 ∧ 𝐶 ∈ ⦋ 𝑧 / 𝑦 ⦌ 𝐴 ) )
29 28 anbi2i ⊢ ( ( 𝑦 ∈ { 𝑧 } ∧ ( 𝐶 ∈ ⦋ 𝑧 / 𝑦 ⦌ 𝐴 ∧ [ 𝑧 / 𝑦 ] 𝑦 ∈ 𝐵 ) ) ↔ ( 𝑦 ∈ { 𝑧 } ∧ ( [ 𝑧 / 𝑦 ] 𝑦 ∈ 𝐵 ∧ 𝐶 ∈ ⦋ 𝑧 / 𝑦 ⦌ 𝐴 ) ) )
30 27 29 bitri ⊢ ( ( [ 𝑧 / 𝑦 ] 𝑦 ∈ 𝐵 ∧ ( 𝐶 ∈ ⦋ 𝑧 / 𝑦 ⦌ 𝐴 ∧ 𝑦 ∈ { 𝑧 } ) ) ↔ ( 𝑦 ∈ { 𝑧 } ∧ ( [ 𝑧 / 𝑦 ] 𝑦 ∈ 𝐵 ∧ 𝐶 ∈ ⦋ 𝑧 / 𝑦 ⦌ 𝐴 ) ) )
31 velsn ⊢ ( 𝑦 ∈ { 𝑧 } ↔ 𝑦 = 𝑧 )
32 equcom ⊢ ( 𝑦 = 𝑧 ↔ 𝑧 = 𝑦 )
33 31 32 bitri ⊢ ( 𝑦 ∈ { 𝑧 } ↔ 𝑧 = 𝑦 )
34 33 anbi1i ⊢ ( ( 𝑦 ∈ { 𝑧 } ∧ ( [ 𝑧 / 𝑦 ] 𝑦 ∈ 𝐵 ∧ 𝐶 ∈ ⦋ 𝑧 / 𝑦 ⦌ 𝐴 ) ) ↔ ( 𝑧 = 𝑦 ∧ ( [ 𝑧 / 𝑦 ] 𝑦 ∈ 𝐵 ∧ 𝐶 ∈ ⦋ 𝑧 / 𝑦 ⦌ 𝐴 ) ) )
35 26 30 34 3bitri ⊢ ( ( [ 𝑧 / 𝑦 ] 𝑦 ∈ 𝐵 ∧ ⟨ 𝐶 , 𝑦 ⟩ ∈ ( ⦋ 𝑧 / 𝑦 ⦌ 𝐴 × { 𝑧 } ) ) ↔ ( 𝑧 = 𝑦 ∧ ( [ 𝑧 / 𝑦 ] 𝑦 ∈ 𝐵 ∧ 𝐶 ∈ ⦋ 𝑧 / 𝑦 ⦌ 𝐴 ) ) )
36 35 exbii ⊢ ( ∃ 𝑧 ( [ 𝑧 / 𝑦 ] 𝑦 ∈ 𝐵 ∧ ⟨ 𝐶 , 𝑦 ⟩ ∈ ( ⦋ 𝑧 / 𝑦 ⦌ 𝐴 × { 𝑧 } ) ) ↔ ∃ 𝑧 ( 𝑧 = 𝑦 ∧ ( [ 𝑧 / 𝑦 ] 𝑦 ∈ 𝐵 ∧ 𝐶 ∈ ⦋ 𝑧 / 𝑦 ⦌ 𝐴 ) ) )
37 sbequ12r ⊢ ( 𝑧 = 𝑦 → ( [ 𝑧 / 𝑦 ] 𝑦 ∈ 𝐵 ↔ 𝑦 ∈ 𝐵 ) )
38 13 equcoms ⊢ ( 𝑧 = 𝑦 → 𝐴 = ⦋ 𝑧 / 𝑦 ⦌ 𝐴 )
39 38 eqcomd ⊢ ( 𝑧 = 𝑦 → ⦋ 𝑧 / 𝑦 ⦌ 𝐴 = 𝐴 )
40 39 eleq2d ⊢ ( 𝑧 = 𝑦 → ( 𝐶 ∈ ⦋ 𝑧 / 𝑦 ⦌ 𝐴 ↔ 𝐶 ∈ 𝐴 ) )
41 37 40 anbi12d ⊢ ( 𝑧 = 𝑦 → ( ( [ 𝑧 / 𝑦 ] 𝑦 ∈ 𝐵 ∧ 𝐶 ∈ ⦋ 𝑧 / 𝑦 ⦌ 𝐴 ) ↔ ( 𝑦 ∈ 𝐵 ∧ 𝐶 ∈ 𝐴 ) ) )
42 41 equsexvw ⊢ ( ∃ 𝑧 ( 𝑧 = 𝑦 ∧ ( [ 𝑧 / 𝑦 ] 𝑦 ∈ 𝐵 ∧ 𝐶 ∈ ⦋ 𝑧 / 𝑦 ⦌ 𝐴 ) ) ↔ ( 𝑦 ∈ 𝐵 ∧ 𝐶 ∈ 𝐴 ) )
43 36 42 bitri ⊢ ( ∃ 𝑧 ( [ 𝑧 / 𝑦 ] 𝑦 ∈ 𝐵 ∧ ⟨ 𝐶 , 𝑦 ⟩ ∈ ( ⦋ 𝑧 / 𝑦 ⦌ 𝐴 × { 𝑧 } ) ) ↔ ( 𝑦 ∈ 𝐵 ∧ 𝐶 ∈ 𝐴 ) )
44 2 24 43 3bitri ⊢ ( ⟨ 𝐶 , 𝑦 ⟩ ∈ ∪ 𝑦 ∈ 𝐵 ( 𝐴 × { 𝑦 } ) ↔ ( 𝑦 ∈ 𝐵 ∧ 𝐶 ∈ 𝐴 ) )