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

Metamath Proof Explorer

Theorem fiss

Description: Subset relationship for function fi . (Contributed by Jeff Hankins, 7-Oct-2009) (Revised by Mario Carneiro, 24-Nov-2013)

Ref Expression
Assertion fiss ⊢ B ∈ V ∧ A ⊆ B → fi ⁡ A ⊆ fi ⁡ B

Proof

Step Hyp Ref Expression
1 sstr2 ⊢ A ⊆ B → B ⊆ y → A ⊆ y
2 1 adantl ⊢ B ∈ V ∧ A ⊆ B → B ⊆ y → A ⊆ y
3 2 anim1d ⊢ B ∈ V ∧ A ⊆ B → B ⊆ y ∧ ∀ x ∈ y ∀ z ∈ y x ∩ z ∈ y → A ⊆ y ∧ ∀ x ∈ y ∀ z ∈ y x ∩ z ∈ y
4 3 ss2abdv ⊢ B ∈ V ∧ A ⊆ B → y | B ⊆ y ∧ ∀ x ∈ y ∀ z ∈ y x ∩ z ∈ y ⊆ y | A ⊆ y ∧ ∀ x ∈ y ∀ z ∈ y x ∩ z ∈ y
5 intss ⊢ y | B ⊆ y ∧ ∀ x ∈ y ∀ z ∈ y x ∩ z ∈ y ⊆ y | A ⊆ y ∧ ∀ x ∈ y ∀ z ∈ y x ∩ z ∈ y → ⋂ y | A ⊆ y ∧ ∀ x ∈ y ∀ z ∈ y x ∩ z ∈ y ⊆ ⋂ y | B ⊆ y ∧ ∀ x ∈ y ∀ z ∈ y x ∩ z ∈ y
6 4 5 syl ⊢ B ∈ V ∧ A ⊆ B → ⋂ y | A ⊆ y ∧ ∀ x ∈ y ∀ z ∈ y x ∩ z ∈ y ⊆ ⋂ y | B ⊆ y ∧ ∀ x ∈ y ∀ z ∈ y x ∩ z ∈ y
7 ssexg ⊢ A ⊆ B ∧ B ∈ V → A ∈ V
8 7 ancoms ⊢ B ∈ V ∧ A ⊆ B → A ∈ V
9 dffi2 ⊢ A ∈ V → fi ⁡ A = ⋂ y | A ⊆ y ∧ ∀ x ∈ y ∀ z ∈ y x ∩ z ∈ y
10 8 9 syl ⊢ B ∈ V ∧ A ⊆ B → fi ⁡ A = ⋂ y | A ⊆ y ∧ ∀ x ∈ y ∀ z ∈ y x ∩ z ∈ y
11 dffi2 ⊢ B ∈ V → fi ⁡ B = ⋂ y | B ⊆ y ∧ ∀ x ∈ y ∀ z ∈ y x ∩ z ∈ y
12 11 adantr ⊢ B ∈ V ∧ A ⊆ B → fi ⁡ B = ⋂ y | B ⊆ y ∧ ∀ x ∈ y ∀ z ∈ y x ∩ z ∈ y
13 6 10 12 3sstr4d ⊢ B ∈ V ∧ A ⊆ B → fi ⁡ A ⊆ fi ⁡ B