Theorem cnvssco

Description: A condition weaker than reflexivity. (Contributed by RP, 3-Aug-2020)

	Ref	Expression
Assertion	cnvssco	⊢ ( ◡ 𝐴 ⊆ ◡ ( 𝐵 ∘ 𝐶 ) ↔ ∀ 𝑥 ∀ 𝑦 ∃ 𝑧 ( 𝑥 𝐴 𝑦 → ( 𝑥 𝐶 𝑧 ∧ 𝑧 𝐵 𝑦 ) ) )

Proof

Step	Hyp	Ref	Expression
1		alcom	⊢ ( ∀ 𝑦 ∀ 𝑥 ( ⟨ 𝑦 , 𝑥 ⟩ ∈ ◡ 𝐴 → ⟨ 𝑦 , 𝑥 ⟩ ∈ ◡ ( 𝐵 ∘ 𝐶 ) ) ↔ ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑦 , 𝑥 ⟩ ∈ ◡ 𝐴 → ⟨ 𝑦 , 𝑥 ⟩ ∈ ◡ ( 𝐵 ∘ 𝐶 ) ) )
2		relcnv	⊢ Rel ◡ 𝐴
3		ssrel	⊢ ( Rel ◡ 𝐴 → ( ◡ 𝐴 ⊆ ◡ ( 𝐵 ∘ 𝐶 ) ↔ ∀ 𝑦 ∀ 𝑥 ( ⟨ 𝑦 , 𝑥 ⟩ ∈ ◡ 𝐴 → ⟨ 𝑦 , 𝑥 ⟩ ∈ ◡ ( 𝐵 ∘ 𝐶 ) ) ) )
4	2 3	ax-mp	⊢ ( ◡ 𝐴 ⊆ ◡ ( 𝐵 ∘ 𝐶 ) ↔ ∀ 𝑦 ∀ 𝑥 ( ⟨ 𝑦 , 𝑥 ⟩ ∈ ◡ 𝐴 → ⟨ 𝑦 , 𝑥 ⟩ ∈ ◡ ( 𝐵 ∘ 𝐶 ) ) )
5		19.37v	⊢ ( ∃ 𝑧 ( 𝑥 𝐴 𝑦 → ( 𝑥 𝐶 𝑧 ∧ 𝑧 𝐵 𝑦 ) ) ↔ ( 𝑥 𝐴 𝑦 → ∃ 𝑧 ( 𝑥 𝐶 𝑧 ∧ 𝑧 𝐵 𝑦 ) ) )
6		vex	⊢ 𝑦 ∈ V
7		vex	⊢ 𝑥 ∈ V
8	6 7	brcnv	⊢ ( 𝑦 ◡ 𝐴 𝑥 ↔ 𝑥 𝐴 𝑦 )
9		df-br	⊢ ( 𝑦 ◡ 𝐴 𝑥 ↔ ⟨ 𝑦 , 𝑥 ⟩ ∈ ◡ 𝐴 )
10	8 9	bitr3i	⊢ ( 𝑥 𝐴 𝑦 ↔ ⟨ 𝑦 , 𝑥 ⟩ ∈ ◡ 𝐴 )
11	7 6	brco	⊢ ( 𝑥 ( 𝐵 ∘ 𝐶 ) 𝑦 ↔ ∃ 𝑧 ( 𝑥 𝐶 𝑧 ∧ 𝑧 𝐵 𝑦 ) )
12	6 7	brcnv	⊢ ( 𝑦 ◡ ( 𝐵 ∘ 𝐶 ) 𝑥 ↔ 𝑥 ( 𝐵 ∘ 𝐶 ) 𝑦 )
13		df-br	⊢ ( 𝑦 ◡ ( 𝐵 ∘ 𝐶 ) 𝑥 ↔ ⟨ 𝑦 , 𝑥 ⟩ ∈ ◡ ( 𝐵 ∘ 𝐶 ) )
14	12 13	bitr3i	⊢ ( 𝑥 ( 𝐵 ∘ 𝐶 ) 𝑦 ↔ ⟨ 𝑦 , 𝑥 ⟩ ∈ ◡ ( 𝐵 ∘ 𝐶 ) )
15	11 14	bitr3i	⊢ ( ∃ 𝑧 ( 𝑥 𝐶 𝑧 ∧ 𝑧 𝐵 𝑦 ) ↔ ⟨ 𝑦 , 𝑥 ⟩ ∈ ◡ ( 𝐵 ∘ 𝐶 ) )
16	10 15	imbi12i	⊢ ( ( 𝑥 𝐴 𝑦 → ∃ 𝑧 ( 𝑥 𝐶 𝑧 ∧ 𝑧 𝐵 𝑦 ) ) ↔ ( ⟨ 𝑦 , 𝑥 ⟩ ∈ ◡ 𝐴 → ⟨ 𝑦 , 𝑥 ⟩ ∈ ◡ ( 𝐵 ∘ 𝐶 ) ) )
17	5 16	bitri	⊢ ( ∃ 𝑧 ( 𝑥 𝐴 𝑦 → ( 𝑥 𝐶 𝑧 ∧ 𝑧 𝐵 𝑦 ) ) ↔ ( ⟨ 𝑦 , 𝑥 ⟩ ∈ ◡ 𝐴 → ⟨ 𝑦 , 𝑥 ⟩ ∈ ◡ ( 𝐵 ∘ 𝐶 ) ) )
18	17	2albii	⊢ ( ∀ 𝑥 ∀ 𝑦 ∃ 𝑧 ( 𝑥 𝐴 𝑦 → ( 𝑥 𝐶 𝑧 ∧ 𝑧 𝐵 𝑦 ) ) ↔ ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑦 , 𝑥 ⟩ ∈ ◡ 𝐴 → ⟨ 𝑦 , 𝑥 ⟩ ∈ ◡ ( 𝐵 ∘ 𝐶 ) ) )
19	1 4 18	3bitr4i	⊢ ( ◡ 𝐴 ⊆ ◡ ( 𝐵 ∘ 𝐶 ) ↔ ∀ 𝑥 ∀ 𝑦 ∃ 𝑧 ( 𝑥 𝐴 𝑦 → ( 𝑥 𝐶 𝑧 ∧ 𝑧 𝐵 𝑦 ) ) )