This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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