Theorem sscoid

Description: A condition for subset and composition with identity. (Contributed by Scott Fenton, 13-Apr-2018)

	Ref	Expression
Assertion	sscoid	⊢ ( 𝐴 ⊆ ( I ∘ 𝐵 ) ↔ ( Rel 𝐴 ∧ 𝐴 ⊆ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		relco	⊢ Rel ( I ∘ 𝐵 )
2		relss	⊢ ( 𝐴 ⊆ ( I ∘ 𝐵 ) → ( Rel ( I ∘ 𝐵 ) → Rel 𝐴 ) )
3	1 2	mpi	⊢ ( 𝐴 ⊆ ( I ∘ 𝐵 ) → Rel 𝐴 )
4		elrel	⊢ ( ( Rel 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑦 ∃ 𝑧 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ )
5		vex	⊢ 𝑦 ∈ V
6		vex	⊢ 𝑧 ∈ V
7	5 6	brco	⊢ ( 𝑦 ( I ∘ 𝐵 ) 𝑧 ↔ ∃ 𝑥 ( 𝑦 𝐵 𝑥 ∧ 𝑥 I 𝑧 ) )
8	6	ideq	⊢ ( 𝑥 I 𝑧 ↔ 𝑥 = 𝑧 )
9	8	anbi1ci	⊢ ( ( 𝑦 𝐵 𝑥 ∧ 𝑥 I 𝑧 ) ↔ ( 𝑥 = 𝑧 ∧ 𝑦 𝐵 𝑥 ) )
10	9	exbii	⊢ ( ∃ 𝑥 ( 𝑦 𝐵 𝑥 ∧ 𝑥 I 𝑧 ) ↔ ∃ 𝑥 ( 𝑥 = 𝑧 ∧ 𝑦 𝐵 𝑥 ) )
11		breq2	⊢ ( 𝑥 = 𝑧 → ( 𝑦 𝐵 𝑥 ↔ 𝑦 𝐵 𝑧 ) )
12	11	equsexvw	⊢ ( ∃ 𝑥 ( 𝑥 = 𝑧 ∧ 𝑦 𝐵 𝑥 ) ↔ 𝑦 𝐵 𝑧 )
13	7 10 12	3bitri	⊢ ( 𝑦 ( I ∘ 𝐵 ) 𝑧 ↔ 𝑦 𝐵 𝑧 )
14	13	a1i	⊢ ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ → ( 𝑦 ( I ∘ 𝐵 ) 𝑧 ↔ 𝑦 𝐵 𝑧 ) )
15		eleq1	⊢ ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ → ( 𝑥 ∈ ( I ∘ 𝐵 ) ↔ ⟨ 𝑦 , 𝑧 ⟩ ∈ ( I ∘ 𝐵 ) ) )
16		df-br	⊢ ( 𝑦 ( I ∘ 𝐵 ) 𝑧 ↔ ⟨ 𝑦 , 𝑧 ⟩ ∈ ( I ∘ 𝐵 ) )
17	15 16	bitr4di	⊢ ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ → ( 𝑥 ∈ ( I ∘ 𝐵 ) ↔ 𝑦 ( I ∘ 𝐵 ) 𝑧 ) )
18		eleq1	⊢ ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ → ( 𝑥 ∈ 𝐵 ↔ ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝐵 ) )
19		df-br	⊢ ( 𝑦 𝐵 𝑧 ↔ ⟨ 𝑦 , 𝑧 ⟩ ∈ 𝐵 )
20	18 19	bitr4di	⊢ ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ → ( 𝑥 ∈ 𝐵 ↔ 𝑦 𝐵 𝑧 ) )
21	14 17 20	3bitr4d	⊢ ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ → ( 𝑥 ∈ ( I ∘ 𝐵 ) ↔ 𝑥 ∈ 𝐵 ) )
22	21	exlimivv	⊢ ( ∃ 𝑦 ∃ 𝑧 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ → ( 𝑥 ∈ ( I ∘ 𝐵 ) ↔ 𝑥 ∈ 𝐵 ) )
23	4 22	syl	⊢ ( ( Rel 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 ∈ ( I ∘ 𝐵 ) ↔ 𝑥 ∈ 𝐵 ) )
24	23	pm5.74da	⊢ ( Rel 𝐴 → ( ( 𝑥 ∈ 𝐴 → 𝑥 ∈ ( I ∘ 𝐵 ) ) ↔ ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) ) )
25	24	albidv	⊢ ( Rel 𝐴 → ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝑥 ∈ ( I ∘ 𝐵 ) ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) ) )
26		df-ss	⊢ ( 𝐴 ⊆ ( I ∘ 𝐵 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝑥 ∈ ( I ∘ 𝐵 ) ) )
27		df-ss	⊢ ( 𝐴 ⊆ 𝐵 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵 ) )
28	25 26 27	3bitr4g	⊢ ( Rel 𝐴 → ( 𝐴 ⊆ ( I ∘ 𝐵 ) ↔ 𝐴 ⊆ 𝐵 ) )
29	3 28	biadanii	⊢ ( 𝐴 ⊆ ( I ∘ 𝐵 ) ↔ ( Rel 𝐴 ∧ 𝐴 ⊆ 𝐵 ) )