Metamath Proof Explorer


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 dfss2 ( 𝐴 ⊆ ( I ∘ 𝐵 ) ↔ ∀ 𝑥 ( 𝑥𝐴𝑥 ∈ ( I ∘ 𝐵 ) ) )
27 dfss2 ( 𝐴𝐵 ↔ ∀ 𝑥 ( 𝑥𝐴𝑥𝐵 ) )
28 25 26 27 3bitr4g ( Rel 𝐴 → ( 𝐴 ⊆ ( I ∘ 𝐵 ) ↔ 𝐴𝐵 ) )
29 3 28 biadanii ( 𝐴 ⊆ ( I ∘ 𝐵 ) ↔ ( Rel 𝐴𝐴𝐵 ) )