Theorem codir

Description: Two ways of saying a relation is directed. (Contributed by Mario Carneiro, 22-Nov-2013)

	Ref	Expression
Assertion	codir	⊢ ( ( 𝐴 × 𝐵 ) ⊆ ( ◡ 𝑅 ∘ 𝑅 ) ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ∃ 𝑧 ( 𝑥 𝑅 𝑧 ∧ 𝑦 𝑅 𝑧 ) )

Proof

Step	Hyp	Ref	Expression
1		opelxp	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 × 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) )
2		df-br	⊢ ( 𝑥 ( ◡ 𝑅 ∘ 𝑅 ) 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ◡ 𝑅 ∘ 𝑅 ) )
3		brcodir	⊢ ( ( 𝑥 ∈ V ∧ 𝑦 ∈ V ) → ( 𝑥 ( ◡ 𝑅 ∘ 𝑅 ) 𝑦 ↔ ∃ 𝑧 ( 𝑥 𝑅 𝑧 ∧ 𝑦 𝑅 𝑧 ) ) )
4	3	el2v	⊢ ( 𝑥 ( ◡ 𝑅 ∘ 𝑅 ) 𝑦 ↔ ∃ 𝑧 ( 𝑥 𝑅 𝑧 ∧ 𝑦 𝑅 𝑧 ) )
5	2 4	bitr3i	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ◡ 𝑅 ∘ 𝑅 ) ↔ ∃ 𝑧 ( 𝑥 𝑅 𝑧 ∧ 𝑦 𝑅 𝑧 ) )
6	1 5	imbi12i	⊢ ( ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 × 𝐵 ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ◡ 𝑅 ∘ 𝑅 ) ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ∃ 𝑧 ( 𝑥 𝑅 𝑧 ∧ 𝑦 𝑅 𝑧 ) ) )
7	6	2albii	⊢ ( ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 × 𝐵 ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ◡ 𝑅 ∘ 𝑅 ) ) ↔ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ∃ 𝑧 ( 𝑥 𝑅 𝑧 ∧ 𝑦 𝑅 𝑧 ) ) )
8		relxp	⊢ Rel ( 𝐴 × 𝐵 )
9		ssrel	⊢ ( Rel ( 𝐴 × 𝐵 ) → ( ( 𝐴 × 𝐵 ) ⊆ ( ◡ 𝑅 ∘ 𝑅 ) ↔ ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 × 𝐵 ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ◡ 𝑅 ∘ 𝑅 ) ) ) )
10	8 9	ax-mp	⊢ ( ( 𝐴 × 𝐵 ) ⊆ ( ◡ 𝑅 ∘ 𝑅 ) ↔ ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( 𝐴 × 𝐵 ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ◡ 𝑅 ∘ 𝑅 ) ) )
11		r2al	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ∃ 𝑧 ( 𝑥 𝑅 𝑧 ∧ 𝑦 𝑅 𝑧 ) ↔ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) → ∃ 𝑧 ( 𝑥 𝑅 𝑧 ∧ 𝑦 𝑅 𝑧 ) ) )
12	7 10 11	3bitr4i	⊢ ( ( 𝐴 × 𝐵 ) ⊆ ( ◡ 𝑅 ∘ 𝑅 ) ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ∃ 𝑧 ( 𝑥 𝑅 𝑧 ∧ 𝑦 𝑅 𝑧 ) )