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 ${⊢}{A}\in \left({B}×{C}\right)↔\left({A}=⟨\bigcap \bigcap {A},\bigcup \mathrm{ran}\left\{{A}\right\}⟩\wedge \left(\bigcap \bigcap {A}\in {B}\wedge \bigcup \mathrm{ran}\left\{{A}\right\}\in {C}\right)\right)$

Proof

Step Hyp Ref Expression
1 elxp ${⊢}{A}\in \left({B}×{C}\right)↔\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({A}=⟨{x},{y}⟩\wedge \left({x}\in {B}\wedge {y}\in {C}\right)\right)$
2 sneq ${⊢}{A}=⟨{x},{y}⟩\to \left\{{A}\right\}=\left\{⟨{x},{y}⟩\right\}$
3 2 rneqd ${⊢}{A}=⟨{x},{y}⟩\to \mathrm{ran}\left\{{A}\right\}=\mathrm{ran}\left\{⟨{x},{y}⟩\right\}$
4 3 unieqd ${⊢}{A}=⟨{x},{y}⟩\to \bigcup \mathrm{ran}\left\{{A}\right\}=\bigcup \mathrm{ran}\left\{⟨{x},{y}⟩\right\}$
5 vex ${⊢}{x}\in \mathrm{V}$
6 vex ${⊢}{y}\in \mathrm{V}$
7 5 6 op2nda ${⊢}\bigcup \mathrm{ran}\left\{⟨{x},{y}⟩\right\}={y}$
8 4 7 syl6req ${⊢}{A}=⟨{x},{y}⟩\to {y}=\bigcup \mathrm{ran}\left\{{A}\right\}$
9 8 pm4.71ri ${⊢}{A}=⟨{x},{y}⟩↔\left({y}=\bigcup \mathrm{ran}\left\{{A}\right\}\wedge {A}=⟨{x},{y}⟩\right)$
10 9 anbi1i ${⊢}\left({A}=⟨{x},{y}⟩\wedge \left({x}\in {B}\wedge {y}\in {C}\right)\right)↔\left(\left({y}=\bigcup \mathrm{ran}\left\{{A}\right\}\wedge {A}=⟨{x},{y}⟩\right)\wedge \left({x}\in {B}\wedge {y}\in {C}\right)\right)$
11 anass ${⊢}\left(\left({y}=\bigcup \mathrm{ran}\left\{{A}\right\}\wedge {A}=⟨{x},{y}⟩\right)\wedge \left({x}\in {B}\wedge {y}\in {C}\right)\right)↔\left({y}=\bigcup \mathrm{ran}\left\{{A}\right\}\wedge \left({A}=⟨{x},{y}⟩\wedge \left({x}\in {B}\wedge {y}\in {C}\right)\right)\right)$
12 10 11 bitri ${⊢}\left({A}=⟨{x},{y}⟩\wedge \left({x}\in {B}\wedge {y}\in {C}\right)\right)↔\left({y}=\bigcup \mathrm{ran}\left\{{A}\right\}\wedge \left({A}=⟨{x},{y}⟩\wedge \left({x}\in {B}\wedge {y}\in {C}\right)\right)\right)$
13 12 exbii ${⊢}\exists {y}\phantom{\rule{.4em}{0ex}}\left({A}=⟨{x},{y}⟩\wedge \left({x}\in {B}\wedge {y}\in {C}\right)\right)↔\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}=\bigcup \mathrm{ran}\left\{{A}\right\}\wedge \left({A}=⟨{x},{y}⟩\wedge \left({x}\in {B}\wedge {y}\in {C}\right)\right)\right)$
14 snex ${⊢}\left\{{A}\right\}\in \mathrm{V}$
15 14 rnex ${⊢}\mathrm{ran}\left\{{A}\right\}\in \mathrm{V}$
16 15 uniex ${⊢}\bigcup \mathrm{ran}\left\{{A}\right\}\in \mathrm{V}$
17 opeq2 ${⊢}{y}=\bigcup \mathrm{ran}\left\{{A}\right\}\to ⟨{x},{y}⟩=⟨{x},\bigcup \mathrm{ran}\left\{{A}\right\}⟩$
18 17 eqeq2d ${⊢}{y}=\bigcup \mathrm{ran}\left\{{A}\right\}\to \left({A}=⟨{x},{y}⟩↔{A}=⟨{x},\bigcup \mathrm{ran}\left\{{A}\right\}⟩\right)$
19 eleq1 ${⊢}{y}=\bigcup \mathrm{ran}\left\{{A}\right\}\to \left({y}\in {C}↔\bigcup \mathrm{ran}\left\{{A}\right\}\in {C}\right)$
20 19 anbi2d ${⊢}{y}=\bigcup \mathrm{ran}\left\{{A}\right\}\to \left(\left({x}\in {B}\wedge {y}\in {C}\right)↔\left({x}\in {B}\wedge \bigcup \mathrm{ran}\left\{{A}\right\}\in {C}\right)\right)$
21 18 20 anbi12d ${⊢}{y}=\bigcup \mathrm{ran}\left\{{A}\right\}\to \left(\left({A}=⟨{x},{y}⟩\wedge \left({x}\in {B}\wedge {y}\in {C}\right)\right)↔\left({A}=⟨{x},\bigcup \mathrm{ran}\left\{{A}\right\}⟩\wedge \left({x}\in {B}\wedge \bigcup \mathrm{ran}\left\{{A}\right\}\in {C}\right)\right)\right)$
22 16 21 ceqsexv ${⊢}\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}=\bigcup \mathrm{ran}\left\{{A}\right\}\wedge \left({A}=⟨{x},{y}⟩\wedge \left({x}\in {B}\wedge {y}\in {C}\right)\right)\right)↔\left({A}=⟨{x},\bigcup \mathrm{ran}\left\{{A}\right\}⟩\wedge \left({x}\in {B}\wedge \bigcup \mathrm{ran}\left\{{A}\right\}\in {C}\right)\right)$
23 13 22 bitri ${⊢}\exists {y}\phantom{\rule{.4em}{0ex}}\left({A}=⟨{x},{y}⟩\wedge \left({x}\in {B}\wedge {y}\in {C}\right)\right)↔\left({A}=⟨{x},\bigcup \mathrm{ran}\left\{{A}\right\}⟩\wedge \left({x}\in {B}\wedge \bigcup \mathrm{ran}\left\{{A}\right\}\in {C}\right)\right)$
24 inteq ${⊢}{A}=⟨{x},\bigcup \mathrm{ran}\left\{{A}\right\}⟩\to \bigcap {A}=\bigcap ⟨{x},\bigcup \mathrm{ran}\left\{{A}\right\}⟩$
25 24 inteqd ${⊢}{A}=⟨{x},\bigcup \mathrm{ran}\left\{{A}\right\}⟩\to \bigcap \bigcap {A}=\bigcap \bigcap ⟨{x},\bigcup \mathrm{ran}\left\{{A}\right\}⟩$
26 5 16 op1stb ${⊢}\bigcap \bigcap ⟨{x},\bigcup \mathrm{ran}\left\{{A}\right\}⟩={x}$
27 25 26 syl6req ${⊢}{A}=⟨{x},\bigcup \mathrm{ran}\left\{{A}\right\}⟩\to {x}=\bigcap \bigcap {A}$
28 27 pm4.71ri ${⊢}{A}=⟨{x},\bigcup \mathrm{ran}\left\{{A}\right\}⟩↔\left({x}=\bigcap \bigcap {A}\wedge {A}=⟨{x},\bigcup \mathrm{ran}\left\{{A}\right\}⟩\right)$
29 28 anbi1i ${⊢}\left({A}=⟨{x},\bigcup \mathrm{ran}\left\{{A}\right\}⟩\wedge \left({x}\in {B}\wedge \bigcup \mathrm{ran}\left\{{A}\right\}\in {C}\right)\right)↔\left(\left({x}=\bigcap \bigcap {A}\wedge {A}=⟨{x},\bigcup \mathrm{ran}\left\{{A}\right\}⟩\right)\wedge \left({x}\in {B}\wedge \bigcup \mathrm{ran}\left\{{A}\right\}\in {C}\right)\right)$
30 anass ${⊢}\left(\left({x}=\bigcap \bigcap {A}\wedge {A}=⟨{x},\bigcup \mathrm{ran}\left\{{A}\right\}⟩\right)\wedge \left({x}\in {B}\wedge \bigcup \mathrm{ran}\left\{{A}\right\}\in {C}\right)\right)↔\left({x}=\bigcap \bigcap {A}\wedge \left({A}=⟨{x},\bigcup \mathrm{ran}\left\{{A}\right\}⟩\wedge \left({x}\in {B}\wedge \bigcup \mathrm{ran}\left\{{A}\right\}\in {C}\right)\right)\right)$
31 23 29 30 3bitri ${⊢}\exists {y}\phantom{\rule{.4em}{0ex}}\left({A}=⟨{x},{y}⟩\wedge \left({x}\in {B}\wedge {y}\in {C}\right)\right)↔\left({x}=\bigcap \bigcap {A}\wedge \left({A}=⟨{x},\bigcup \mathrm{ran}\left\{{A}\right\}⟩\wedge \left({x}\in {B}\wedge \bigcup \mathrm{ran}\left\{{A}\right\}\in {C}\right)\right)\right)$
32 31 exbii ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({A}=⟨{x},{y}⟩\wedge \left({x}\in {B}\wedge {y}\in {C}\right)\right)↔\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}=\bigcap \bigcap {A}\wedge \left({A}=⟨{x},\bigcup \mathrm{ran}\left\{{A}\right\}⟩\wedge \left({x}\in {B}\wedge \bigcup \mathrm{ran}\left\{{A}\right\}\in {C}\right)\right)\right)$
33 eqvisset ${⊢}{x}=\bigcap \bigcap {A}\to \bigcap \bigcap {A}\in \mathrm{V}$
34 33 adantr ${⊢}\left({x}=\bigcap \bigcap {A}\wedge \left({A}=⟨{x},\bigcup \mathrm{ran}\left\{{A}\right\}⟩\wedge \left({x}\in {B}\wedge \bigcup \mathrm{ran}\left\{{A}\right\}\in {C}\right)\right)\right)\to \bigcap \bigcap {A}\in \mathrm{V}$
35 34 exlimiv ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}=\bigcap \bigcap {A}\wedge \left({A}=⟨{x},\bigcup \mathrm{ran}\left\{{A}\right\}⟩\wedge \left({x}\in {B}\wedge \bigcup \mathrm{ran}\left\{{A}\right\}\in {C}\right)\right)\right)\to \bigcap \bigcap {A}\in \mathrm{V}$
36 elex ${⊢}\bigcap \bigcap {A}\in {B}\to \bigcap \bigcap {A}\in \mathrm{V}$
37 36 ad2antrl ${⊢}\left({A}=⟨\bigcap \bigcap {A},\bigcup \mathrm{ran}\left\{{A}\right\}⟩\wedge \left(\bigcap \bigcap {A}\in {B}\wedge \bigcup \mathrm{ran}\left\{{A}\right\}\in {C}\right)\right)\to \bigcap \bigcap {A}\in \mathrm{V}$
38 opeq1 ${⊢}{x}=\bigcap \bigcap {A}\to ⟨{x},\bigcup \mathrm{ran}\left\{{A}\right\}⟩=⟨\bigcap \bigcap {A},\bigcup \mathrm{ran}\left\{{A}\right\}⟩$
39 38 eqeq2d ${⊢}{x}=\bigcap \bigcap {A}\to \left({A}=⟨{x},\bigcup \mathrm{ran}\left\{{A}\right\}⟩↔{A}=⟨\bigcap \bigcap {A},\bigcup \mathrm{ran}\left\{{A}\right\}⟩\right)$
40 eleq1 ${⊢}{x}=\bigcap \bigcap {A}\to \left({x}\in {B}↔\bigcap \bigcap {A}\in {B}\right)$
41 40 anbi1d ${⊢}{x}=\bigcap \bigcap {A}\to \left(\left({x}\in {B}\wedge \bigcup \mathrm{ran}\left\{{A}\right\}\in {C}\right)↔\left(\bigcap \bigcap {A}\in {B}\wedge \bigcup \mathrm{ran}\left\{{A}\right\}\in {C}\right)\right)$
42 39 41 anbi12d ${⊢}{x}=\bigcap \bigcap {A}\to \left(\left({A}=⟨{x},\bigcup \mathrm{ran}\left\{{A}\right\}⟩\wedge \left({x}\in {B}\wedge \bigcup \mathrm{ran}\left\{{A}\right\}\in {C}\right)\right)↔\left({A}=⟨\bigcap \bigcap {A},\bigcup \mathrm{ran}\left\{{A}\right\}⟩\wedge \left(\bigcap \bigcap {A}\in {B}\wedge \bigcup \mathrm{ran}\left\{{A}\right\}\in {C}\right)\right)\right)$
43 42 ceqsexgv ${⊢}\bigcap \bigcap {A}\in \mathrm{V}\to \left(\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}=\bigcap \bigcap {A}\wedge \left({A}=⟨{x},\bigcup \mathrm{ran}\left\{{A}\right\}⟩\wedge \left({x}\in {B}\wedge \bigcup \mathrm{ran}\left\{{A}\right\}\in {C}\right)\right)\right)↔\left({A}=⟨\bigcap \bigcap {A},\bigcup \mathrm{ran}\left\{{A}\right\}⟩\wedge \left(\bigcap \bigcap {A}\in {B}\wedge \bigcup \mathrm{ran}\left\{{A}\right\}\in {C}\right)\right)\right)$
44 35 37 43 pm5.21nii ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}=\bigcap \bigcap {A}\wedge \left({A}=⟨{x},\bigcup \mathrm{ran}\left\{{A}\right\}⟩\wedge \left({x}\in {B}\wedge \bigcup \mathrm{ran}\left\{{A}\right\}\in {C}\right)\right)\right)↔\left({A}=⟨\bigcap \bigcap {A},\bigcup \mathrm{ran}\left\{{A}\right\}⟩\wedge \left(\bigcap \bigcap {A}\in {B}\wedge \bigcup \mathrm{ran}\left\{{A}\right\}\in {C}\right)\right)$
45 1 32 44 3bitri ${⊢}{A}\in \left({B}×{C}\right)↔\left({A}=⟨\bigcap \bigcap {A},\bigcup \mathrm{ran}\left\{{A}\right\}⟩\wedge \left(\bigcap \bigcap {A}\in {B}\wedge \bigcup \mathrm{ran}\left\{{A}\right\}\in {C}\right)\right)$