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

Metamath Proof Explorer

Theorem elxp5

Description: Membership in a Cartesian product requiring no quantifiers or dummy variables. Provides a slightly shorter version of elxp4 when the double intersection does not create class existence problems (caused by int0 ). (Contributed by NM, 1-Aug-2004)

Ref Expression
Assertion elxp5 ( 𝐴 ∈ ( 𝐵 × 𝐶 ) ↔ ( 𝐴 = ⟨ ∩ ∩ 𝐴 , ∪ ran { 𝐴 } ⟩ ∧ ( ∩ ∩ 𝐴 ∈ 𝐵 ∧ ∪ 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 inteq ⊢ ( 𝐴 = ⟨ 𝑥 , ∪ ran { 𝐴 } ⟩ → ∩ 𝐴 = ∩ ⟨ 𝑥 , ∪ ran { 𝐴 } ⟩ )
25 24 inteqd ⊢ ( 𝐴 = ⟨ 𝑥 , ∪ ran { 𝐴 } ⟩ → ∩ ∩ 𝐴 = ∩ ∩ ⟨ 𝑥 , ∪ ran { 𝐴 } ⟩ )
26 5 16 op1stb ⊢ ∩ ∩ ⟨ 𝑥 , ∪ ran { 𝐴 } ⟩ = 𝑥
27 25 26 eqtr2di ⊢ ( 𝐴 = ⟨ 𝑥 , ∪ ran { 𝐴 } ⟩ → 𝑥 = ∩ ∩ 𝐴 )
28 27 pm4.71ri ⊢ ( 𝐴 = ⟨ 𝑥 , ∪ ran { 𝐴 } ⟩ ↔ ( 𝑥 = ∩ ∩ 𝐴 ∧ 𝐴 = ⟨ 𝑥 , ∪ ran { 𝐴 } ⟩ ) )
29 28 anbi1i ⊢ ( ( 𝐴 = ⟨ 𝑥 , ∪ ran { 𝐴 } ⟩ ∧ ( 𝑥 ∈ 𝐵 ∧ ∪ ran { 𝐴 } ∈ 𝐶 ) ) ↔ ( ( 𝑥 = ∩ ∩ 𝐴 ∧ 𝐴 = ⟨ 𝑥 , ∪ ran { 𝐴 } ⟩ ) ∧ ( 𝑥 ∈ 𝐵 ∧ ∪ ran { 𝐴 } ∈ 𝐶 ) ) )
30 anass ⊢ ( ( ( 𝑥 = ∩ ∩ 𝐴 ∧ 𝐴 = ⟨ 𝑥 , ∪ ran { 𝐴 } ⟩ ) ∧ ( 𝑥 ∈ 𝐵 ∧ ∪ ran { 𝐴 } ∈ 𝐶 ) ) ↔ ( 𝑥 = ∩ ∩ 𝐴 ∧ ( 𝐴 = ⟨ 𝑥 , ∪ ran { 𝐴 } ⟩ ∧ ( 𝑥 ∈ 𝐵 ∧ ∪ ran { 𝐴 } ∈ 𝐶 ) ) ) )
31 23 29 30 3bitri ⊢ ( ∃ 𝑦 ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) ↔ ( 𝑥 = ∩ ∩ 𝐴 ∧ ( 𝐴 = ⟨ 𝑥 , ∪ ran { 𝐴 } ⟩ ∧ ( 𝑥 ∈ 𝐵 ∧ ∪ ran { 𝐴 } ∈ 𝐶 ) ) ) )
32 31 exbii ⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐶 ) ) ↔ ∃ 𝑥 ( 𝑥 = ∩ ∩ 𝐴 ∧ ( 𝐴 = ⟨ 𝑥 , ∪ ran { 𝐴 } ⟩ ∧ ( 𝑥 ∈ 𝐵 ∧ ∪ ran { 𝐴 } ∈ 𝐶 ) ) ) )
33 eqvisset ⊢ ( 𝑥 = ∩ ∩ 𝐴 → ∩ ∩ 𝐴 ∈ V )
34 33 adantr ⊢ ( ( 𝑥 = ∩ ∩ 𝐴 ∧ ( 𝐴 = ⟨ 𝑥 , ∪ ran { 𝐴 } ⟩ ∧ ( 𝑥 ∈ 𝐵 ∧ ∪ ran { 𝐴 } ∈ 𝐶 ) ) ) → ∩ ∩ 𝐴 ∈ V )
35 34 exlimiv ⊢ ( ∃ 𝑥 ( 𝑥 = ∩ ∩ 𝐴 ∧ ( 𝐴 = ⟨ 𝑥 , ∪ ran { 𝐴 } ⟩ ∧ ( 𝑥 ∈ 𝐵 ∧ ∪ ran { 𝐴 } ∈ 𝐶 ) ) ) → ∩ ∩ 𝐴 ∈ V )
36 elex ⊢ ( ∩ ∩ 𝐴 ∈ 𝐵 → ∩ ∩ 𝐴 ∈ V )
37 36 ad2antrl ⊢ ( ( 𝐴 = ⟨ ∩ ∩ 𝐴 , ∪ ran { 𝐴 } ⟩ ∧ ( ∩ ∩ 𝐴 ∈ 𝐵 ∧ ∪ ran { 𝐴 } ∈ 𝐶 ) ) → ∩ ∩ 𝐴 ∈ V )
38 opeq1 ⊢ ( 𝑥 = ∩ ∩ 𝐴 → ⟨ 𝑥 , ∪ ran { 𝐴 } ⟩ = ⟨ ∩ ∩ 𝐴 , ∪ ran { 𝐴 } ⟩ )
39 38 eqeq2d ⊢ ( 𝑥 = ∩ ∩ 𝐴 → ( 𝐴 = ⟨ 𝑥 , ∪ ran { 𝐴 } ⟩ ↔ 𝐴 = ⟨ ∩ ∩ 𝐴 , ∪ ran { 𝐴 } ⟩ ) )
40 eleq1 ⊢ ( 𝑥 = ∩ ∩ 𝐴 → ( 𝑥 ∈ 𝐵 ↔ ∩ ∩ 𝐴 ∈ 𝐵 ) )
41 40 anbi1d ⊢ ( 𝑥 = ∩ ∩ 𝐴 → ( ( 𝑥 ∈ 𝐵 ∧ ∪ ran { 𝐴 } ∈ 𝐶 ) ↔ ( ∩ ∩ 𝐴 ∈ 𝐵 ∧ ∪ ran { 𝐴 } ∈ 𝐶 ) ) )
42 39 41 anbi12d ⊢ ( 𝑥 = ∩ ∩ 𝐴 → ( ( 𝐴 = ⟨ 𝑥 , ∪ ran { 𝐴 } ⟩ ∧ ( 𝑥 ∈ 𝐵 ∧ ∪ ran { 𝐴 } ∈ 𝐶 ) ) ↔ ( 𝐴 = ⟨ ∩ ∩ 𝐴 , ∪ ran { 𝐴 } ⟩ ∧ ( ∩ ∩ 𝐴 ∈ 𝐵 ∧ ∪ ran { 𝐴 } ∈ 𝐶 ) ) ) )
43 42 ceqsexgv ⊢ ( ∩ ∩ 𝐴 ∈ V → ( ∃ 𝑥 ( 𝑥 = ∩ ∩ 𝐴 ∧ ( 𝐴 = ⟨ 𝑥 , ∪ ran { 𝐴 } ⟩ ∧ ( 𝑥 ∈ 𝐵 ∧ ∪ ran { 𝐴 } ∈ 𝐶 ) ) ) ↔ ( 𝐴 = ⟨ ∩ ∩ 𝐴 , ∪ ran { 𝐴 } ⟩ ∧ ( ∩ ∩ 𝐴 ∈ 𝐵 ∧ ∪ ran { 𝐴 } ∈ 𝐶 ) ) ) )
44 35 37 43 pm5.21nii ⊢ ( ∃ 𝑥 ( 𝑥 = ∩ ∩ 𝐴 ∧ ( 𝐴 = ⟨ 𝑥 , ∪ ran { 𝐴 } ⟩ ∧ ( 𝑥 ∈ 𝐵 ∧ ∪ ran { 𝐴 } ∈ 𝐶 ) ) ) ↔ ( 𝐴 = ⟨ ∩ ∩ 𝐴 , ∪ ran { 𝐴 } ⟩ ∧ ( ∩ ∩ 𝐴 ∈ 𝐵 ∧ ∪ ran { 𝐴 } ∈ 𝐶 ) ) )
45 1 32 44 3bitri ⊢ ( 𝐴 ∈ ( 𝐵 × 𝐶 ) ↔ ( 𝐴 = ⟨ ∩ ∩ 𝐴 , ∪ ran { 𝐴 } ⟩ ∧ ( ∩ ∩ 𝐴 ∈ 𝐵 ∧ ∪ ran { 𝐴 } ∈ 𝐶 ) ) )