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