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

Metamath Proof Explorer

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 { 𝐴 } ∈ 𝐶 ) ) )