Theorem dminxp

Description: Two ways to express totality of a restricted and corestricted binary relation (intersection of a binary relation with a Cartesian product). (Contributed by NM, 17-Jan-2006)

	Ref	Expression
Assertion	dminxp	⊢ ( dom ( 𝐶 ∩ ( 𝐴 × 𝐵 ) ) = 𝐴 ↔ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 𝐶 𝑦 )

Proof

Step	Hyp	Ref	Expression
1		dfdm4	⊢ dom ( 𝐶 ∩ ( 𝐴 × 𝐵 ) ) = ran ◡ ( 𝐶 ∩ ( 𝐴 × 𝐵 ) )
2		cnvin	⊢ ◡ ( 𝐶 ∩ ( 𝐴 × 𝐵 ) ) = ( ◡ 𝐶 ∩ ◡ ( 𝐴 × 𝐵 ) )
3		cnvxp	⊢ ◡ ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 )
4	3	ineq2i	⊢ ( ◡ 𝐶 ∩ ◡ ( 𝐴 × 𝐵 ) ) = ( ◡ 𝐶 ∩ ( 𝐵 × 𝐴 ) )
5	2 4	eqtri	⊢ ◡ ( 𝐶 ∩ ( 𝐴 × 𝐵 ) ) = ( ◡ 𝐶 ∩ ( 𝐵 × 𝐴 ) )
6	5	rneqi	⊢ ran ◡ ( 𝐶 ∩ ( 𝐴 × 𝐵 ) ) = ran ( ◡ 𝐶 ∩ ( 𝐵 × 𝐴 ) )
7	1 6	eqtri	⊢ dom ( 𝐶 ∩ ( 𝐴 × 𝐵 ) ) = ran ( ◡ 𝐶 ∩ ( 𝐵 × 𝐴 ) )
8	7	eqeq1i	⊢ ( dom ( 𝐶 ∩ ( 𝐴 × 𝐵 ) ) = 𝐴 ↔ ran ( ◡ 𝐶 ∩ ( 𝐵 × 𝐴 ) ) = 𝐴 )
9		rninxp	⊢ ( ran ( ◡ 𝐶 ∩ ( 𝐵 × 𝐴 ) ) = 𝐴 ↔ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑦 ◡ 𝐶 𝑥 )
10		vex	⊢ 𝑦 ∈ V
11		vex	⊢ 𝑥 ∈ V
12	10 11	brcnv	⊢ ( 𝑦 ◡ 𝐶 𝑥 ↔ 𝑥 𝐶 𝑦 )
13	12	rexbii	⊢ ( ∃ 𝑦 ∈ 𝐵 𝑦 ◡ 𝐶 𝑥 ↔ ∃ 𝑦 ∈ 𝐵 𝑥 𝐶 𝑦 )
14	13	ralbii	⊢ ( ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑦 ◡ 𝐶 𝑥 ↔ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 𝐶 𝑦 )
15	8 9 14	3bitri	⊢ ( dom ( 𝐶 ∩ ( 𝐴 × 𝐵 ) ) = 𝐴 ↔ ∀ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑥 𝐶 𝑦 )