Metamath Proof Explorer


Theorem brxrn

Description: Characterize a ternary relation over a range Cartesian product. Together with xrnss3v , this characterizes elementhood in a range cross. (Contributed by Peter Mazsa, 27-Jun-2021)

Ref Expression
Assertion brxrn ( ( 𝐴𝑉𝐵𝑊𝐶𝑋 ) → ( 𝐴 ( 𝑅𝑆 ) ⟨ 𝐵 , 𝐶 ⟩ ↔ ( 𝐴 𝑅 𝐵𝐴 𝑆 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 df-xrn ( 𝑅𝑆 ) = ( ( ( 1st ↾ ( V × V ) ) ∘ 𝑅 ) ∩ ( ( 2nd ↾ ( V × V ) ) ∘ 𝑆 ) )
2 1 breqi ( 𝐴 ( 𝑅𝑆 ) ⟨ 𝐵 , 𝐶 ⟩ ↔ 𝐴 ( ( ( 1st ↾ ( V × V ) ) ∘ 𝑅 ) ∩ ( ( 2nd ↾ ( V × V ) ) ∘ 𝑆 ) ) ⟨ 𝐵 , 𝐶 ⟩ )
3 2 a1i ( ( 𝐴𝑉𝐵𝑊𝐶𝑋 ) → ( 𝐴 ( 𝑅𝑆 ) ⟨ 𝐵 , 𝐶 ⟩ ↔ 𝐴 ( ( ( 1st ↾ ( V × V ) ) ∘ 𝑅 ) ∩ ( ( 2nd ↾ ( V × V ) ) ∘ 𝑆 ) ) ⟨ 𝐵 , 𝐶 ⟩ ) )
4 brin ( 𝐴 ( ( ( 1st ↾ ( V × V ) ) ∘ 𝑅 ) ∩ ( ( 2nd ↾ ( V × V ) ) ∘ 𝑆 ) ) ⟨ 𝐵 , 𝐶 ⟩ ↔ ( 𝐴 ( ( 1st ↾ ( V × V ) ) ∘ 𝑅 ) ⟨ 𝐵 , 𝐶 ⟩ ∧ 𝐴 ( ( 2nd ↾ ( V × V ) ) ∘ 𝑆 ) ⟨ 𝐵 , 𝐶 ⟩ ) )
5 4 a1i ( ( 𝐴𝑉𝐵𝑊𝐶𝑋 ) → ( 𝐴 ( ( ( 1st ↾ ( V × V ) ) ∘ 𝑅 ) ∩ ( ( 2nd ↾ ( V × V ) ) ∘ 𝑆 ) ) ⟨ 𝐵 , 𝐶 ⟩ ↔ ( 𝐴 ( ( 1st ↾ ( V × V ) ) ∘ 𝑅 ) ⟨ 𝐵 , 𝐶 ⟩ ∧ 𝐴 ( ( 2nd ↾ ( V × V ) ) ∘ 𝑆 ) ⟨ 𝐵 , 𝐶 ⟩ ) ) )
6 opex 𝐵 , 𝐶 ⟩ ∈ V
7 brcog ( ( 𝐴𝑉 ∧ ⟨ 𝐵 , 𝐶 ⟩ ∈ V ) → ( 𝐴 ( ( 1st ↾ ( V × V ) ) ∘ 𝑅 ) ⟨ 𝐵 , 𝐶 ⟩ ↔ ∃ 𝑥 ( 𝐴 𝑅 𝑥𝑥 ( 1st ↾ ( V × V ) ) ⟨ 𝐵 , 𝐶 ⟩ ) ) )
8 6 7 mpan2 ( 𝐴𝑉 → ( 𝐴 ( ( 1st ↾ ( V × V ) ) ∘ 𝑅 ) ⟨ 𝐵 , 𝐶 ⟩ ↔ ∃ 𝑥 ( 𝐴 𝑅 𝑥𝑥 ( 1st ↾ ( V × V ) ) ⟨ 𝐵 , 𝐶 ⟩ ) ) )
9 8 3ad2ant1 ( ( 𝐴𝑉𝐵𝑊𝐶𝑋 ) → ( 𝐴 ( ( 1st ↾ ( V × V ) ) ∘ 𝑅 ) ⟨ 𝐵 , 𝐶 ⟩ ↔ ∃ 𝑥 ( 𝐴 𝑅 𝑥𝑥 ( 1st ↾ ( V × V ) ) ⟨ 𝐵 , 𝐶 ⟩ ) ) )
10 brcnvg ( ( 𝑥 ∈ V ∧ ⟨ 𝐵 , 𝐶 ⟩ ∈ V ) → ( 𝑥 ( 1st ↾ ( V × V ) ) ⟨ 𝐵 , 𝐶 ⟩ ↔ ⟨ 𝐵 , 𝐶 ⟩ ( 1st ↾ ( V × V ) ) 𝑥 ) )
11 6 10 mpan2 ( 𝑥 ∈ V → ( 𝑥 ( 1st ↾ ( V × V ) ) ⟨ 𝐵 , 𝐶 ⟩ ↔ ⟨ 𝐵 , 𝐶 ⟩ ( 1st ↾ ( V × V ) ) 𝑥 ) )
12 11 elv ( 𝑥 ( 1st ↾ ( V × V ) ) ⟨ 𝐵 , 𝐶 ⟩ ↔ ⟨ 𝐵 , 𝐶 ⟩ ( 1st ↾ ( V × V ) ) 𝑥 )
13 brres ( 𝑥 ∈ V → ( ⟨ 𝐵 , 𝐶 ⟩ ( 1st ↾ ( V × V ) ) 𝑥 ↔ ( ⟨ 𝐵 , 𝐶 ⟩ ∈ ( V × V ) ∧ ⟨ 𝐵 , 𝐶 ⟩ 1st 𝑥 ) ) )
14 13 elv ( ⟨ 𝐵 , 𝐶 ⟩ ( 1st ↾ ( V × V ) ) 𝑥 ↔ ( ⟨ 𝐵 , 𝐶 ⟩ ∈ ( V × V ) ∧ ⟨ 𝐵 , 𝐶 ⟩ 1st 𝑥 ) )
15 opelvvg ( ( 𝐵𝑊𝐶𝑋 ) → ⟨ 𝐵 , 𝐶 ⟩ ∈ ( V × V ) )
16 15 biantrurd ( ( 𝐵𝑊𝐶𝑋 ) → ( ⟨ 𝐵 , 𝐶 ⟩ 1st 𝑥 ↔ ( ⟨ 𝐵 , 𝐶 ⟩ ∈ ( V × V ) ∧ ⟨ 𝐵 , 𝐶 ⟩ 1st 𝑥 ) ) )
17 14 16 bitr4id ( ( 𝐵𝑊𝐶𝑋 ) → ( ⟨ 𝐵 , 𝐶 ⟩ ( 1st ↾ ( V × V ) ) 𝑥 ↔ ⟨ 𝐵 , 𝐶 ⟩ 1st 𝑥 ) )
18 br1steqg ( ( 𝐵𝑊𝐶𝑋 ) → ( ⟨ 𝐵 , 𝐶 ⟩ 1st 𝑥𝑥 = 𝐵 ) )
19 17 18 bitrd ( ( 𝐵𝑊𝐶𝑋 ) → ( ⟨ 𝐵 , 𝐶 ⟩ ( 1st ↾ ( V × V ) ) 𝑥𝑥 = 𝐵 ) )
20 19 3adant1 ( ( 𝐴𝑉𝐵𝑊𝐶𝑋 ) → ( ⟨ 𝐵 , 𝐶 ⟩ ( 1st ↾ ( V × V ) ) 𝑥𝑥 = 𝐵 ) )
21 12 20 syl5bb ( ( 𝐴𝑉𝐵𝑊𝐶𝑋 ) → ( 𝑥 ( 1st ↾ ( V × V ) ) ⟨ 𝐵 , 𝐶 ⟩ ↔ 𝑥 = 𝐵 ) )
22 21 anbi1cd ( ( 𝐴𝑉𝐵𝑊𝐶𝑋 ) → ( ( 𝐴 𝑅 𝑥𝑥 ( 1st ↾ ( V × V ) ) ⟨ 𝐵 , 𝐶 ⟩ ) ↔ ( 𝑥 = 𝐵𝐴 𝑅 𝑥 ) ) )
23 22 exbidv ( ( 𝐴𝑉𝐵𝑊𝐶𝑋 ) → ( ∃ 𝑥 ( 𝐴 𝑅 𝑥𝑥 ( 1st ↾ ( V × V ) ) ⟨ 𝐵 , 𝐶 ⟩ ) ↔ ∃ 𝑥 ( 𝑥 = 𝐵𝐴 𝑅 𝑥 ) ) )
24 breq2 ( 𝑥 = 𝐵 → ( 𝐴 𝑅 𝑥𝐴 𝑅 𝐵 ) )
25 24 ceqsexgv ( 𝐵𝑊 → ( ∃ 𝑥 ( 𝑥 = 𝐵𝐴 𝑅 𝑥 ) ↔ 𝐴 𝑅 𝐵 ) )
26 25 3ad2ant2 ( ( 𝐴𝑉𝐵𝑊𝐶𝑋 ) → ( ∃ 𝑥 ( 𝑥 = 𝐵𝐴 𝑅 𝑥 ) ↔ 𝐴 𝑅 𝐵 ) )
27 9 23 26 3bitrd ( ( 𝐴𝑉𝐵𝑊𝐶𝑋 ) → ( 𝐴 ( ( 1st ↾ ( V × V ) ) ∘ 𝑅 ) ⟨ 𝐵 , 𝐶 ⟩ ↔ 𝐴 𝑅 𝐵 ) )
28 brcog ( ( 𝐴𝑉 ∧ ⟨ 𝐵 , 𝐶 ⟩ ∈ V ) → ( 𝐴 ( ( 2nd ↾ ( V × V ) ) ∘ 𝑆 ) ⟨ 𝐵 , 𝐶 ⟩ ↔ ∃ 𝑦 ( 𝐴 𝑆 𝑦𝑦 ( 2nd ↾ ( V × V ) ) ⟨ 𝐵 , 𝐶 ⟩ ) ) )
29 6 28 mpan2 ( 𝐴𝑉 → ( 𝐴 ( ( 2nd ↾ ( V × V ) ) ∘ 𝑆 ) ⟨ 𝐵 , 𝐶 ⟩ ↔ ∃ 𝑦 ( 𝐴 𝑆 𝑦𝑦 ( 2nd ↾ ( V × V ) ) ⟨ 𝐵 , 𝐶 ⟩ ) ) )
30 29 3ad2ant1 ( ( 𝐴𝑉𝐵𝑊𝐶𝑋 ) → ( 𝐴 ( ( 2nd ↾ ( V × V ) ) ∘ 𝑆 ) ⟨ 𝐵 , 𝐶 ⟩ ↔ ∃ 𝑦 ( 𝐴 𝑆 𝑦𝑦 ( 2nd ↾ ( V × V ) ) ⟨ 𝐵 , 𝐶 ⟩ ) ) )
31 brcnvg ( ( 𝑦 ∈ V ∧ ⟨ 𝐵 , 𝐶 ⟩ ∈ V ) → ( 𝑦 ( 2nd ↾ ( V × V ) ) ⟨ 𝐵 , 𝐶 ⟩ ↔ ⟨ 𝐵 , 𝐶 ⟩ ( 2nd ↾ ( V × V ) ) 𝑦 ) )
32 6 31 mpan2 ( 𝑦 ∈ V → ( 𝑦 ( 2nd ↾ ( V × V ) ) ⟨ 𝐵 , 𝐶 ⟩ ↔ ⟨ 𝐵 , 𝐶 ⟩ ( 2nd ↾ ( V × V ) ) 𝑦 ) )
33 32 elv ( 𝑦 ( 2nd ↾ ( V × V ) ) ⟨ 𝐵 , 𝐶 ⟩ ↔ ⟨ 𝐵 , 𝐶 ⟩ ( 2nd ↾ ( V × V ) ) 𝑦 )
34 brres ( 𝑦 ∈ V → ( ⟨ 𝐵 , 𝐶 ⟩ ( 2nd ↾ ( V × V ) ) 𝑦 ↔ ( ⟨ 𝐵 , 𝐶 ⟩ ∈ ( V × V ) ∧ ⟨ 𝐵 , 𝐶 ⟩ 2nd 𝑦 ) ) )
35 34 elv ( ⟨ 𝐵 , 𝐶 ⟩ ( 2nd ↾ ( V × V ) ) 𝑦 ↔ ( ⟨ 𝐵 , 𝐶 ⟩ ∈ ( V × V ) ∧ ⟨ 𝐵 , 𝐶 ⟩ 2nd 𝑦 ) )
36 15 biantrurd ( ( 𝐵𝑊𝐶𝑋 ) → ( ⟨ 𝐵 , 𝐶 ⟩ 2nd 𝑦 ↔ ( ⟨ 𝐵 , 𝐶 ⟩ ∈ ( V × V ) ∧ ⟨ 𝐵 , 𝐶 ⟩ 2nd 𝑦 ) ) )
37 35 36 bitr4id ( ( 𝐵𝑊𝐶𝑋 ) → ( ⟨ 𝐵 , 𝐶 ⟩ ( 2nd ↾ ( V × V ) ) 𝑦 ↔ ⟨ 𝐵 , 𝐶 ⟩ 2nd 𝑦 ) )
38 br2ndeqg ( ( 𝐵𝑊𝐶𝑋 ) → ( ⟨ 𝐵 , 𝐶 ⟩ 2nd 𝑦𝑦 = 𝐶 ) )
39 37 38 bitrd ( ( 𝐵𝑊𝐶𝑋 ) → ( ⟨ 𝐵 , 𝐶 ⟩ ( 2nd ↾ ( V × V ) ) 𝑦𝑦 = 𝐶 ) )
40 39 3adant1 ( ( 𝐴𝑉𝐵𝑊𝐶𝑋 ) → ( ⟨ 𝐵 , 𝐶 ⟩ ( 2nd ↾ ( V × V ) ) 𝑦𝑦 = 𝐶 ) )
41 33 40 syl5bb ( ( 𝐴𝑉𝐵𝑊𝐶𝑋 ) → ( 𝑦 ( 2nd ↾ ( V × V ) ) ⟨ 𝐵 , 𝐶 ⟩ ↔ 𝑦 = 𝐶 ) )
42 41 anbi1cd ( ( 𝐴𝑉𝐵𝑊𝐶𝑋 ) → ( ( 𝐴 𝑆 𝑦𝑦 ( 2nd ↾ ( V × V ) ) ⟨ 𝐵 , 𝐶 ⟩ ) ↔ ( 𝑦 = 𝐶𝐴 𝑆 𝑦 ) ) )
43 42 exbidv ( ( 𝐴𝑉𝐵𝑊𝐶𝑋 ) → ( ∃ 𝑦 ( 𝐴 𝑆 𝑦𝑦 ( 2nd ↾ ( V × V ) ) ⟨ 𝐵 , 𝐶 ⟩ ) ↔ ∃ 𝑦 ( 𝑦 = 𝐶𝐴 𝑆 𝑦 ) ) )
44 breq2 ( 𝑦 = 𝐶 → ( 𝐴 𝑆 𝑦𝐴 𝑆 𝐶 ) )
45 44 ceqsexgv ( 𝐶𝑋 → ( ∃ 𝑦 ( 𝑦 = 𝐶𝐴 𝑆 𝑦 ) ↔ 𝐴 𝑆 𝐶 ) )
46 45 3ad2ant3 ( ( 𝐴𝑉𝐵𝑊𝐶𝑋 ) → ( ∃ 𝑦 ( 𝑦 = 𝐶𝐴 𝑆 𝑦 ) ↔ 𝐴 𝑆 𝐶 ) )
47 30 43 46 3bitrd ( ( 𝐴𝑉𝐵𝑊𝐶𝑋 ) → ( 𝐴 ( ( 2nd ↾ ( V × V ) ) ∘ 𝑆 ) ⟨ 𝐵 , 𝐶 ⟩ ↔ 𝐴 𝑆 𝐶 ) )
48 27 47 anbi12d ( ( 𝐴𝑉𝐵𝑊𝐶𝑋 ) → ( ( 𝐴 ( ( 1st ↾ ( V × V ) ) ∘ 𝑅 ) ⟨ 𝐵 , 𝐶 ⟩ ∧ 𝐴 ( ( 2nd ↾ ( V × V ) ) ∘ 𝑆 ) ⟨ 𝐵 , 𝐶 ⟩ ) ↔ ( 𝐴 𝑅 𝐵𝐴 𝑆 𝐶 ) ) )
49 3 5 48 3bitrd ( ( 𝐴𝑉𝐵𝑊𝐶𝑋 ) → ( 𝐴 ( 𝑅𝑆 ) ⟨ 𝐵 , 𝐶 ⟩ ↔ ( 𝐴 𝑅 𝐵𝐴 𝑆 𝐶 ) ) )