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