brtxp

Description: Characterize a ternary relation over a tail Cartesian product. Together with txpss3v , this completely defines membership in a tail cross. (Contributed by Scott Fenton, 31-Mar-2012) (Proof shortened by Peter Mazsa, 2-Oct-2022)

	Ref	Expression
Hypotheses	brtxp.1	⊢ 𝑋 ∈ V
	brtxp.2	⊢ 𝑌 ∈ V
	brtxp.3	⊢ 𝑍 ∈ V
Assertion	brtxp	⊢ ( 𝑋 ( 𝐴 ⊗ 𝐵 ) ⟨ 𝑌 , 𝑍 ⟩ ↔ ( 𝑋 𝐴 𝑌 ∧ 𝑋 𝐵 𝑍 ) )

Proof

Step	Hyp	Ref	Expression
1		brtxp.1	⊢ 𝑋 ∈ V
2		brtxp.2	⊢ 𝑌 ∈ V
3		brtxp.3	⊢ 𝑍 ∈ V
4		df-txp	⊢ ( 𝐴 ⊗ 𝐵 ) = ( ( ^◡ ( 1^st ↾ ( V × V ) ) ∘ 𝐴 ) ∩ ( ^◡ ( 2^nd ↾ ( V × V ) ) ∘ 𝐵 ) )
5	4	breqi	⊢ ( 𝑋 ( 𝐴 ⊗ 𝐵 ) ⟨ 𝑌 , 𝑍 ⟩ ↔ 𝑋 ( ( ^◡ ( 1^st ↾ ( V × V ) ) ∘ 𝐴 ) ∩ ( ^◡ ( 2^nd ↾ ( V × V ) ) ∘ 𝐵 ) ) ⟨ 𝑌 , 𝑍 ⟩ )
6		brin	⊢ ( 𝑋 ( ( ^◡ ( 1^st ↾ ( V × V ) ) ∘ 𝐴 ) ∩ ( ^◡ ( 2^nd ↾ ( V × V ) ) ∘ 𝐵 ) ) ⟨ 𝑌 , 𝑍 ⟩ ↔ ( 𝑋 ( ^◡ ( 1^st ↾ ( V × V ) ) ∘ 𝐴 ) ⟨ 𝑌 , 𝑍 ⟩ ∧ 𝑋 ( ^◡ ( 2^nd ↾ ( V × V ) ) ∘ 𝐵 ) ⟨ 𝑌 , 𝑍 ⟩ ) )
7		opex	⊢ ⟨ 𝑌 , 𝑍 ⟩ ∈ V
8	1 7	brco	⊢ ( 𝑋 ( ^◡ ( 1^st ↾ ( V × V ) ) ∘ 𝐴 ) ⟨ 𝑌 , 𝑍 ⟩ ↔ ∃ 𝑦 ( 𝑋 𝐴 𝑦 ∧ 𝑦 ^◡ ( 1^st ↾ ( V × V ) ) ⟨ 𝑌 , 𝑍 ⟩ ) )
9		vex	⊢ 𝑦 ∈ V
10	9 7	brcnv	⊢ ( 𝑦 ^◡ ( 1^st ↾ ( V × V ) ) ⟨ 𝑌 , 𝑍 ⟩ ↔ ⟨ 𝑌 , 𝑍 ⟩ ( 1^st ↾ ( V × V ) ) 𝑦 )
11	2 3	opelvv	⊢ ⟨ 𝑌 , 𝑍 ⟩ ∈ ( V × V )
12	9	brresi	⊢ ( ⟨ 𝑌 , 𝑍 ⟩ ( 1^st ↾ ( V × V ) ) 𝑦 ↔ ( ⟨ 𝑌 , 𝑍 ⟩ ∈ ( V × V ) ∧ ⟨ 𝑌 , 𝑍 ⟩ 1^st 𝑦 ) )
13	11 12	mpbiran	⊢ ( ⟨ 𝑌 , 𝑍 ⟩ ( 1^st ↾ ( V × V ) ) 𝑦 ↔ ⟨ 𝑌 , 𝑍 ⟩ 1^st 𝑦 )
14	2 3	br1steq	⊢ ( ⟨ 𝑌 , 𝑍 ⟩ 1^st 𝑦 ↔ 𝑦 = 𝑌 )
15	10 13 14	3bitri	⊢ ( 𝑦 ^◡ ( 1^st ↾ ( V × V ) ) ⟨ 𝑌 , 𝑍 ⟩ ↔ 𝑦 = 𝑌 )
16	15	anbi1ci	⊢ ( ( 𝑋 𝐴 𝑦 ∧ 𝑦 ^◡ ( 1^st ↾ ( V × V ) ) ⟨ 𝑌 , 𝑍 ⟩ ) ↔ ( 𝑦 = 𝑌 ∧ 𝑋 𝐴 𝑦 ) )
17	16	exbii	⊢ ( ∃ 𝑦 ( 𝑋 𝐴 𝑦 ∧ 𝑦 ^◡ ( 1^st ↾ ( V × V ) ) ⟨ 𝑌 , 𝑍 ⟩ ) ↔ ∃ 𝑦 ( 𝑦 = 𝑌 ∧ 𝑋 𝐴 𝑦 ) )
18		breq2	⊢ ( 𝑦 = 𝑌 → ( 𝑋 𝐴 𝑦 ↔ 𝑋 𝐴 𝑌 ) )
19	2 18	ceqsexv	⊢ ( ∃ 𝑦 ( 𝑦 = 𝑌 ∧ 𝑋 𝐴 𝑦 ) ↔ 𝑋 𝐴 𝑌 )
20	8 17 19	3bitri	⊢ ( 𝑋 ( ^◡ ( 1^st ↾ ( V × V ) ) ∘ 𝐴 ) ⟨ 𝑌 , 𝑍 ⟩ ↔ 𝑋 𝐴 𝑌 )
21	1 7	brco	⊢ ( 𝑋 ( ^◡ ( 2^nd ↾ ( V × V ) ) ∘ 𝐵 ) ⟨ 𝑌 , 𝑍 ⟩ ↔ ∃ 𝑧 ( 𝑋 𝐵 𝑧 ∧ 𝑧 ^◡ ( 2^nd ↾ ( V × V ) ) ⟨ 𝑌 , 𝑍 ⟩ ) )
22		vex	⊢ 𝑧 ∈ V
23	22 7	brcnv	⊢ ( 𝑧 ^◡ ( 2^nd ↾ ( V × V ) ) ⟨ 𝑌 , 𝑍 ⟩ ↔ ⟨ 𝑌 , 𝑍 ⟩ ( 2^nd ↾ ( V × V ) ) 𝑧 )
24	22	brresi	⊢ ( ⟨ 𝑌 , 𝑍 ⟩ ( 2^nd ↾ ( V × V ) ) 𝑧 ↔ ( ⟨ 𝑌 , 𝑍 ⟩ ∈ ( V × V ) ∧ ⟨ 𝑌 , 𝑍 ⟩ 2^nd 𝑧 ) )
25	11 24	mpbiran	⊢ ( ⟨ 𝑌 , 𝑍 ⟩ ( 2^nd ↾ ( V × V ) ) 𝑧 ↔ ⟨ 𝑌 , 𝑍 ⟩ 2^nd 𝑧 )
26	2 3	br2ndeq	⊢ ( ⟨ 𝑌 , 𝑍 ⟩ 2^nd 𝑧 ↔ 𝑧 = 𝑍 )
27	23 25 26	3bitri	⊢ ( 𝑧 ^◡ ( 2^nd ↾ ( V × V ) ) ⟨ 𝑌 , 𝑍 ⟩ ↔ 𝑧 = 𝑍 )
28	27	anbi1ci	⊢ ( ( 𝑋 𝐵 𝑧 ∧ 𝑧 ^◡ ( 2^nd ↾ ( V × V ) ) ⟨ 𝑌 , 𝑍 ⟩ ) ↔ ( 𝑧 = 𝑍 ∧ 𝑋 𝐵 𝑧 ) )
29	28	exbii	⊢ ( ∃ 𝑧 ( 𝑋 𝐵 𝑧 ∧ 𝑧 ^◡ ( 2^nd ↾ ( V × V ) ) ⟨ 𝑌 , 𝑍 ⟩ ) ↔ ∃ 𝑧 ( 𝑧 = 𝑍 ∧ 𝑋 𝐵 𝑧 ) )
30		breq2	⊢ ( 𝑧 = 𝑍 → ( 𝑋 𝐵 𝑧 ↔ 𝑋 𝐵 𝑍 ) )
31	3 30	ceqsexv	⊢ ( ∃ 𝑧 ( 𝑧 = 𝑍 ∧ 𝑋 𝐵 𝑧 ) ↔ 𝑋 𝐵 𝑍 )
32	21 29 31	3bitri	⊢ ( 𝑋 ( ^◡ ( 2^nd ↾ ( V × V ) ) ∘ 𝐵 ) ⟨ 𝑌 , 𝑍 ⟩ ↔ 𝑋 𝐵 𝑍 )
33	20 32	anbi12i	⊢ ( ( 𝑋 ( ^◡ ( 1^st ↾ ( V × V ) ) ∘ 𝐴 ) ⟨ 𝑌 , 𝑍 ⟩ ∧ 𝑋 ( ^◡ ( 2^nd ↾ ( V × V ) ) ∘ 𝐵 ) ⟨ 𝑌 , 𝑍 ⟩ ) ↔ ( 𝑋 𝐴 𝑌 ∧ 𝑋 𝐵 𝑍 ) )
34	5 6 33	3bitri	⊢ ( 𝑋 ( 𝐴 ⊗ 𝐵 ) ⟨ 𝑌 , 𝑍 ⟩ ↔ ( 𝑋 𝐴 𝑌 ∧ 𝑋 𝐵 𝑍 ) )

Metamath Proof Explorer

Theorem brtxp

Proof