Theorem elxp4

Description: Membership in a Cartesian product. This version requires no quantifiers or dummy variables. See also elxp5 , elxp6 , and elxp7 . (Contributed by NM, 17-Feb-2004)

	Ref	Expression
Assertion	elxp4	⊢ ( 𝐴 ∈ ( 𝐵 × 𝐶 ) ↔ ( 𝐴 = ⟨ ∪ dom { 𝐴 } , ∪ ran { 𝐴 } ⟩ ∧ ( ∪ dom { 𝐴 } ∈ 𝐵 ∧ ∪ ran { 𝐴 } ∈ 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		elxp	⊢ ( 𝐴 ∈ ( 𝐵 × 𝐶 ) ↔ ∃ 𝑥 ∃ 𝑦 ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) )
2		sneq	⊢ ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ → { 𝐴 } = { ⟨ 𝑥 , 𝑦 ⟩ } )
3	2	rneqd	⊢ ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ → ran { 𝐴 } = ran { ⟨ 𝑥 , 𝑦 ⟩ } )
4	3	unieqd	⊢ ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ → ∪ ran { 𝐴 } = ∪ ran { ⟨ 𝑥 , 𝑦 ⟩ } )
5		vex	⊢ 𝑥 ∈ V
6		vex	⊢ 𝑦 ∈ V
7	5 6	op2nda	⊢ ∪ ran { ⟨ 𝑥 , 𝑦 ⟩ } = 𝑦
8	4 7	eqtr2di	⊢ ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ → 𝑦 = ∪ ran { 𝐴 } )
9	8	pm4.71ri	⊢ ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ↔ ( 𝑦 = ∪ ran { 𝐴 } ∧ 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ) )
10	9	anbi1i	⊢ ( ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) ↔ ( ( 𝑦 = ∪ ran { 𝐴 } ∧ 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) )
11		anass	⊢ ( ( ( 𝑦 = ∪ ran { 𝐴 } ∧ 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) ↔ ( 𝑦 = ∪ ran { 𝐴 } ∧ ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) ) )
12	10 11	bitri	⊢ ( ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) ↔ ( 𝑦 = ∪ ran { 𝐴 } ∧ ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) ) )
13	12	exbii	⊢ ( ∃ 𝑦 ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) ↔ ∃ 𝑦 ( 𝑦 = ∪ ran { 𝐴 } ∧ ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) ) )
14		snex	⊢ { 𝐴 } ∈ V
15	14	rnex	⊢ ran { 𝐴 } ∈ V
16	15	uniex	⊢ ∪ ran { 𝐴 } ∈ V
17		opeq2	⊢ ( 𝑦 = ∪ ran { 𝐴 } → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑥 , ∪ ran { 𝐴 } ⟩ )
18	17	eqeq2d	⊢ ( 𝑦 = ∪ ran { 𝐴 } → ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ↔ 𝐴 = ⟨ 𝑥 , ∪ ran { 𝐴 } ⟩ ) )
19		eleq1	⊢ ( 𝑦 = ∪ ran { 𝐴 } → ( 𝑦 ∈ 𝐶 ↔ ∪ ran { 𝐴 } ∈ 𝐶 ) )
20	19	anbi2d	⊢ ( 𝑦 = ∪ ran { 𝐴 } → ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ↔ ( 𝑥 ∈ 𝐵 ∧ ∪ ran { 𝐴 } ∈ 𝐶 ) ) )
21	18 20	anbi12d	⊢ ( 𝑦 = ∪ ran { 𝐴 } → ( ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) ↔ ( 𝐴 = ⟨ 𝑥 , ∪ ran { 𝐴 } ⟩ ∧ ( 𝑥 ∈ 𝐵 ∧ ∪ ran { 𝐴 } ∈ 𝐶 ) ) ) )
22	16 21	ceqsexv	⊢ ( ∃ 𝑦 ( 𝑦 = ∪ ran { 𝐴 } ∧ ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) ) ↔ ( 𝐴 = ⟨ 𝑥 , ∪ ran { 𝐴 } ⟩ ∧ ( 𝑥 ∈ 𝐵 ∧ ∪ ran { 𝐴 } ∈ 𝐶 ) ) )
23	13 22	bitri	⊢ ( ∃ 𝑦 ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) ↔ ( 𝐴 = ⟨ 𝑥 , ∪ ran { 𝐴 } ⟩ ∧ ( 𝑥 ∈ 𝐵 ∧ ∪ ran { 𝐴 } ∈ 𝐶 ) ) )
24		sneq	⊢ ( 𝐴 = ⟨ 𝑥 , ∪ ran { 𝐴 } ⟩ → { 𝐴 } = { ⟨ 𝑥 , ∪ ran { 𝐴 } ⟩ } )
25	24	dmeqd	⊢ ( 𝐴 = ⟨ 𝑥 , ∪ ran { 𝐴 } ⟩ → dom { 𝐴 } = dom { ⟨ 𝑥 , ∪ ran { 𝐴 } ⟩ } )
26	25	unieqd	⊢ ( 𝐴 = ⟨ 𝑥 , ∪ ran { 𝐴 } ⟩ → ∪ dom { 𝐴 } = ∪ dom { ⟨ 𝑥 , ∪ ran { 𝐴 } ⟩ } )
27	5 16	op1sta	⊢ ∪ dom { ⟨ 𝑥 , ∪ ran { 𝐴 } ⟩ } = 𝑥
28	26 27	eqtr2di	⊢ ( 𝐴 = ⟨ 𝑥 , ∪ ran { 𝐴 } ⟩ → 𝑥 = ∪ dom { 𝐴 } )
29	28	pm4.71ri	⊢ ( 𝐴 = ⟨ 𝑥 , ∪ ran { 𝐴 } ⟩ ↔ ( 𝑥 = ∪ dom { 𝐴 } ∧ 𝐴 = ⟨ 𝑥 , ∪ ran { 𝐴 } ⟩ ) )
30	29	anbi1i	⊢ ( ( 𝐴 = ⟨ 𝑥 , ∪ ran { 𝐴 } ⟩ ∧ ( 𝑥 ∈ 𝐵 ∧ ∪ ran { 𝐴 } ∈ 𝐶 ) ) ↔ ( ( 𝑥 = ∪ dom { 𝐴 } ∧ 𝐴 = ⟨ 𝑥 , ∪ ran { 𝐴 } ⟩ ) ∧ ( 𝑥 ∈ 𝐵 ∧ ∪ ran { 𝐴 } ∈ 𝐶 ) ) )
31		anass	⊢ ( ( ( 𝑥 = ∪ dom { 𝐴 } ∧ 𝐴 = ⟨ 𝑥 , ∪ ran { 𝐴 } ⟩ ) ∧ ( 𝑥 ∈ 𝐵 ∧ ∪ ran { 𝐴 } ∈ 𝐶 ) ) ↔ ( 𝑥 = ∪ dom { 𝐴 } ∧ ( 𝐴 = ⟨ 𝑥 , ∪ ran { 𝐴 } ⟩ ∧ ( 𝑥 ∈ 𝐵 ∧ ∪ ran { 𝐴 } ∈ 𝐶 ) ) ) )
32	23 30 31	3bitri	⊢ ( ∃ 𝑦 ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) ↔ ( 𝑥 = ∪ dom { 𝐴 } ∧ ( 𝐴 = ⟨ 𝑥 , ∪ ran { 𝐴 } ⟩ ∧ ( 𝑥 ∈ 𝐵 ∧ ∪ ran { 𝐴 } ∈ 𝐶 ) ) ) )
33	32	exbii	⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) ↔ ∃ 𝑥 ( 𝑥 = ∪ dom { 𝐴 } ∧ ( 𝐴 = ⟨ 𝑥 , ∪ ran { 𝐴 } ⟩ ∧ ( 𝑥 ∈ 𝐵 ∧ ∪ ran { 𝐴 } ∈ 𝐶 ) ) ) )
34	14	dmex	⊢ dom { 𝐴 } ∈ V
35	34	uniex	⊢ ∪ dom { 𝐴 } ∈ V
36		opeq1	⊢ ( 𝑥 = ∪ dom { 𝐴 } → ⟨ 𝑥 , ∪ ran { 𝐴 } ⟩ = ⟨ ∪ dom { 𝐴 } , ∪ ran { 𝐴 } ⟩ )
37	36	eqeq2d	⊢ ( 𝑥 = ∪ dom { 𝐴 } → ( 𝐴 = ⟨ 𝑥 , ∪ ran { 𝐴 } ⟩ ↔ 𝐴 = ⟨ ∪ dom { 𝐴 } , ∪ ran { 𝐴 } ⟩ ) )
38		eleq1	⊢ ( 𝑥 = ∪ dom { 𝐴 } → ( 𝑥 ∈ 𝐵 ↔ ∪ dom { 𝐴 } ∈ 𝐵 ) )
39	38	anbi1d	⊢ ( 𝑥 = ∪ dom { 𝐴 } → ( ( 𝑥 ∈ 𝐵 ∧ ∪ ran { 𝐴 } ∈ 𝐶 ) ↔ ( ∪ dom { 𝐴 } ∈ 𝐵 ∧ ∪ ran { 𝐴 } ∈ 𝐶 ) ) )
40	37 39	anbi12d	⊢ ( 𝑥 = ∪ dom { 𝐴 } → ( ( 𝐴 = ⟨ 𝑥 , ∪ ran { 𝐴 } ⟩ ∧ ( 𝑥 ∈ 𝐵 ∧ ∪ ran { 𝐴 } ∈ 𝐶 ) ) ↔ ( 𝐴 = ⟨ ∪ dom { 𝐴 } , ∪ ran { 𝐴 } ⟩ ∧ ( ∪ dom { 𝐴 } ∈ 𝐵 ∧ ∪ ran { 𝐴 } ∈ 𝐶 ) ) ) )
41	35 40	ceqsexv	⊢ ( ∃ 𝑥 ( 𝑥 = ∪ dom { 𝐴 } ∧ ( 𝐴 = ⟨ 𝑥 , ∪ ran { 𝐴 } ⟩ ∧ ( 𝑥 ∈ 𝐵 ∧ ∪ ran { 𝐴 } ∈ 𝐶 ) ) ) ↔ ( 𝐴 = ⟨ ∪ dom { 𝐴 } , ∪ ran { 𝐴 } ⟩ ∧ ( ∪ dom { 𝐴 } ∈ 𝐵 ∧ ∪ ran { 𝐴 } ∈ 𝐶 ) ) )
42	1 33 41	3bitri	⊢ ( 𝐴 ∈ ( 𝐵 × 𝐶 ) ↔ ( 𝐴 = ⟨ ∪ dom { 𝐴 } , ∪ ran { 𝐴 } ⟩ ∧ ( ∪ dom { 𝐴 } ∈ 𝐵 ∧ ∪ ran { 𝐴 } ∈ 𝐶 ) ) )