Theorem refimssco

Description: Reflexive relations are subsets of their self-composition. (Contributed by RP, 4-Aug-2020)

	Ref	Expression
Assertion	refimssco	⊢ ( ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) ⊆ 𝐴 → ◡ 𝐴 ⊆ ◡ ( 𝐴 ∘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		breq2	⊢ ( 𝑧 = 𝑥 → ( 𝑥 𝐴 𝑧 ↔ 𝑥 𝐴 𝑥 ) )
2		breq1	⊢ ( 𝑧 = 𝑥 → ( 𝑧 𝐴 𝑦 ↔ 𝑥 𝐴 𝑦 ) )
3	1 2	anbi12d	⊢ ( 𝑧 = 𝑥 → ( ( 𝑥 𝐴 𝑧 ∧ 𝑧 𝐴 𝑦 ) ↔ ( 𝑥 𝐴 𝑥 ∧ 𝑥 𝐴 𝑦 ) ) )
4	3	biimprd	⊢ ( 𝑧 = 𝑥 → ( ( 𝑥 𝐴 𝑥 ∧ 𝑥 𝐴 𝑦 ) → ( 𝑥 𝐴 𝑧 ∧ 𝑧 𝐴 𝑦 ) ) )
5	4	spimevw	⊢ ( ( 𝑥 𝐴 𝑥 ∧ 𝑥 𝐴 𝑦 ) → ∃ 𝑧 ( 𝑥 𝐴 𝑧 ∧ 𝑧 𝐴 𝑦 ) )
6	5	ex	⊢ ( 𝑥 𝐴 𝑥 → ( 𝑥 𝐴 𝑦 → ∃ 𝑧 ( 𝑥 𝐴 𝑧 ∧ 𝑧 𝐴 𝑦 ) ) )
7	6	adantr	⊢ ( ( 𝑥 𝐴 𝑥 ∧ 𝑦 𝐴 𝑦 ) → ( 𝑥 𝐴 𝑦 → ∃ 𝑧 ( 𝑥 𝐴 𝑧 ∧ 𝑧 𝐴 𝑦 ) ) )
8	7	com12	⊢ ( 𝑥 𝐴 𝑦 → ( ( 𝑥 𝐴 𝑥 ∧ 𝑦 𝐴 𝑦 ) → ∃ 𝑧 ( 𝑥 𝐴 𝑧 ∧ 𝑧 𝐴 𝑦 ) ) )
9	8	a2i	⊢ ( ( 𝑥 𝐴 𝑦 → ( 𝑥 𝐴 𝑥 ∧ 𝑦 𝐴 𝑦 ) ) → ( 𝑥 𝐴 𝑦 → ∃ 𝑧 ( 𝑥 𝐴 𝑧 ∧ 𝑧 𝐴 𝑦 ) ) )
10		19.37v	⊢ ( ∃ 𝑧 ( 𝑥 𝐴 𝑦 → ( 𝑥 𝐴 𝑧 ∧ 𝑧 𝐴 𝑦 ) ) ↔ ( 𝑥 𝐴 𝑦 → ∃ 𝑧 ( 𝑥 𝐴 𝑧 ∧ 𝑧 𝐴 𝑦 ) ) )
11	9 10	sylibr	⊢ ( ( 𝑥 𝐴 𝑦 → ( 𝑥 𝐴 𝑥 ∧ 𝑦 𝐴 𝑦 ) ) → ∃ 𝑧 ( 𝑥 𝐴 𝑦 → ( 𝑥 𝐴 𝑧 ∧ 𝑧 𝐴 𝑦 ) ) )
12	11	2alimi	⊢ ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝐴 𝑦 → ( 𝑥 𝐴 𝑥 ∧ 𝑦 𝐴 𝑦 ) ) → ∀ 𝑥 ∀ 𝑦 ∃ 𝑧 ( 𝑥 𝐴 𝑦 → ( 𝑥 𝐴 𝑧 ∧ 𝑧 𝐴 𝑦 ) ) )
13		reflexg	⊢ ( ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) ⊆ 𝐴 ↔ ∀ 𝑥 ∀ 𝑦 ( 𝑥 𝐴 𝑦 → ( 𝑥 𝐴 𝑥 ∧ 𝑦 𝐴 𝑦 ) ) )
14		cnvssco	⊢ ( ◡ 𝐴 ⊆ ◡ ( 𝐴 ∘ 𝐴 ) ↔ ∀ 𝑥 ∀ 𝑦 ∃ 𝑧 ( 𝑥 𝐴 𝑦 → ( 𝑥 𝐴 𝑧 ∧ 𝑧 𝐴 𝑦 ) ) )
15	12 13 14	3imtr4i	⊢ ( ( I ↾ ( dom 𝐴 ∪ ran 𝐴 ) ) ⊆ 𝐴 → ◡ 𝐴 ⊆ ◡ ( 𝐴 ∘ 𝐴 ) )