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

Metamath Proof Explorer

Theorem imagesset

Description: The Image functor applied to the converse of the subset relationship yields a subset of the subset relationship. (Contributed by Scott Fenton, 14-Apr-2018)

Ref Expression
Assertion imagesset Image ◡ SSet ⊆ SSet

Proof

Step Hyp Ref Expression
1 ssid ⊢ 𝑦 ⊆ 𝑦
2 sseq2 ⊢ ( 𝑧 = 𝑦 → ( 𝑦 ⊆ 𝑧 ↔ 𝑦 ⊆ 𝑦 ) )
3 2 rspcev ⊢ ( ( 𝑦 ∈ 𝑥 ∧ 𝑦 ⊆ 𝑦 ) → ∃ 𝑧 ∈ 𝑥 𝑦 ⊆ 𝑧 )
4 1 3 mpan2 ⊢ ( 𝑦 ∈ 𝑥 → ∃ 𝑧 ∈ 𝑥 𝑦 ⊆ 𝑧 )
5 vex ⊢ 𝑦 ∈ V
6 5 elima ⊢ ( 𝑦 ∈ ( ◡ SSet “ 𝑥 ) ↔ ∃ 𝑧 ∈ 𝑥 𝑧 ◡ SSet 𝑦 )
7 vex ⊢ 𝑧 ∈ V
8 7 5 brcnv ⊢ ( 𝑧 ◡ SSet 𝑦 ↔ 𝑦 SSet 𝑧 )
9 7 brsset ⊢ ( 𝑦 SSet 𝑧 ↔ 𝑦 ⊆ 𝑧 )
10 8 9 bitri ⊢ ( 𝑧 ◡ SSet 𝑦 ↔ 𝑦 ⊆ 𝑧 )
11 10 rexbii ⊢ ( ∃ 𝑧 ∈ 𝑥 𝑧 ◡ SSet 𝑦 ↔ ∃ 𝑧 ∈ 𝑥 𝑦 ⊆ 𝑧 )
12 6 11 bitri ⊢ ( 𝑦 ∈ ( ◡ SSet “ 𝑥 ) ↔ ∃ 𝑧 ∈ 𝑥 𝑦 ⊆ 𝑧 )
13 4 12 sylibr ⊢ ( 𝑦 ∈ 𝑥 → 𝑦 ∈ ( ◡ SSet “ 𝑥 ) )
14 13 ssriv ⊢ 𝑥 ⊆ ( ◡ SSet “ 𝑥 )
15 sseq2 ⊢ ( 𝑦 = ( ◡ SSet “ 𝑥 ) → ( 𝑥 ⊆ 𝑦 ↔ 𝑥 ⊆ ( ◡ SSet “ 𝑥 ) ) )
16 14 15 mpbiri ⊢ ( 𝑦 = ( ◡ SSet “ 𝑥 ) → 𝑥 ⊆ 𝑦 )
17 vex ⊢ 𝑥 ∈ V
18 17 5 brimage ⊢ ( 𝑥 Image ◡ SSet 𝑦 ↔ 𝑦 = ( ◡ SSet “ 𝑥 ) )
19 df-br ⊢ ( 𝑥 Image ◡ SSet 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ Image ◡ SSet )
20 18 19 bitr3i ⊢ ( 𝑦 = ( ◡ SSet “ 𝑥 ) ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ Image ◡ SSet )
21 5 brsset ⊢ ( 𝑥 SSet 𝑦 ↔ 𝑥 ⊆ 𝑦 )
22 df-br ⊢ ( 𝑥 SSet 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ SSet )
23 21 22 bitr3i ⊢ ( 𝑥 ⊆ 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ SSet )
24 16 20 23 3imtr3i ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ Image ◡ SSet → ⟨ 𝑥 , 𝑦 ⟩ ∈ SSet )
25 24 gen2 ⊢ ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ Image ◡ SSet → ⟨ 𝑥 , 𝑦 ⟩ ∈ SSet )
26 funimage ⊢ Fun Image ◡ SSet
27 funrel ⊢ ( Fun Image ◡ SSet → Rel Image ◡ SSet )
28 ssrel ⊢ ( Rel Image ◡ SSet → ( Image ◡ SSet ⊆ SSet ↔ ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ Image ◡ SSet → ⟨ 𝑥 , 𝑦 ⟩ ∈ SSet ) ) )
29 26 27 28 mp2b ⊢ ( Image ◡ SSet ⊆ SSet ↔ ∀ 𝑥 ∀ 𝑦 ( ⟨ 𝑥 , 𝑦 ⟩ ∈ Image ◡ SSet → ⟨ 𝑥 , 𝑦 ⟩ ∈ SSet ) )
30 25 29 mpbir ⊢ Image ◡ SSet ⊆ SSet