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	⊢ ( ⟨ 𝐶 , 𝑦 ⟩ ∈ ∪ 𝑦 ∈ 𝐵 ( 𝐴 × { 𝑦 } ) ↔ ( 𝑦 ∈ 𝐵 ∧ 𝐶 ∈ 𝐴 ) )