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

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 bitrid ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → ( 𝑥 ◡ ( 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 bitrid ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → ( 𝑦 ◡ ( 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 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ 𝐶 ∈ 𝑋 ) → ( 𝐴 ( 𝑅 ⋉ 𝑆 ) ⟨ 𝐵 , 𝐶 ⟩ ↔ ( 𝐴 𝑅 𝐵 ∧ 𝐴 𝑆 𝐶 ) ) )