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

Metamath Proof Explorer

Theorem bnj548

Description: Technical lemma for bnj852 . This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

Ref Expression
Hypotheses bnj548.1 No typesetting found for |- ( ta <-> ( f Fn m /\ ph' /\ ps' ) ) with typecode |-
bnj548.2 ⊢ B = ⋃ y ∈ f ⁡ i pred y A R
bnj548.3 ⊢ K = ⋃ y ∈ G ⁡ i pred y A R
bnj548.4 ⊢ G = f ∪ m C
bnj548.5 ⊢ R FrSe A ∧ τ ∧ σ → G Fn n
Assertion bnj548 ⊢ R FrSe A ∧ τ ∧ σ ∧ i ∈ m → B = K

Proof

Step Hyp Ref Expression
1 bnj548.1 Could not format ( ta <-> ( f Fn m /\ ph' /\ ps' ) ) : No typesetting found for |- ( ta <-> ( f Fn m /\ ph' /\ ps' ) ) with typecode |-
2 bnj548.2 ⊢ B = ⋃ y ∈ f ⁡ i pred y A R
3 bnj548.3 ⊢ K = ⋃ y ∈ G ⁡ i pred y A R
4 bnj548.4 ⊢ G = f ∪ m C
5 bnj548.5 ⊢ R FrSe A ∧ τ ∧ σ → G Fn n
6 5 fnfund ⊢ R FrSe A ∧ τ ∧ σ → Fun ⁡ G
7 6 adantr ⊢ R FrSe A ∧ τ ∧ σ ∧ i ∈ m → Fun ⁡ G
8 1 simp1bi ⊢ τ → f Fn m
9 fndm ⊢ f Fn m → dom ⁡ f = m
10 eleq2 ⊢ dom ⁡ f = m → i ∈ dom ⁡ f ↔ i ∈ m
11 10 biimpar ⊢ dom ⁡ f = m ∧ i ∈ m → i ∈ dom ⁡ f
12 9 11 sylan ⊢ f Fn m ∧ i ∈ m → i ∈ dom ⁡ f
13 8 12 sylan ⊢ τ ∧ i ∈ m → i ∈ dom ⁡ f
14 13 3ad2antl2 ⊢ R FrSe A ∧ τ ∧ σ ∧ i ∈ m → i ∈ dom ⁡ f
15 7 14 jca ⊢ R FrSe A ∧ τ ∧ σ ∧ i ∈ m → Fun ⁡ G ∧ i ∈ dom ⁡ f
16 4 bnj931 ⊢ f ⊆ G
17 15 16 jctil ⊢ R FrSe A ∧ τ ∧ σ ∧ i ∈ m → f ⊆ G ∧ Fun ⁡ G ∧ i ∈ dom ⁡ f
18 3anan12 ⊢ Fun ⁡ G ∧ f ⊆ G ∧ i ∈ dom ⁡ f ↔ f ⊆ G ∧ Fun ⁡ G ∧ i ∈ dom ⁡ f
19 17 18 sylibr ⊢ R FrSe A ∧ τ ∧ σ ∧ i ∈ m → Fun ⁡ G ∧ f ⊆ G ∧ i ∈ dom ⁡ f
20 funssfv ⊢ Fun ⁡ G ∧ f ⊆ G ∧ i ∈ dom ⁡ f → G ⁡ i = f ⁡ i
21 iuneq1 ⊢ G ⁡ i = f ⁡ i → ⋃ y ∈ G ⁡ i pred y A R = ⋃ y ∈ f ⁡ i pred y A R
22 21 eqcomd ⊢ G ⁡ i = f ⁡ i → ⋃ y ∈ f ⁡ i pred y A R = ⋃ y ∈ G ⁡ i pred y A R
23 22 2 3 3eqtr4g ⊢ G ⁡ i = f ⁡ i → B = K
24 19 20 23 3syl ⊢ R FrSe A ∧ τ ∧ σ ∧ i ∈ m → B = K