Metamath Proof Explorer

Theorem bnj535

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 bnj535.1 No typesetting found for |- ( ph' <-> ( f ` (/) ) = _pred ( x , A , R ) ) with typecode |-
bnj535.2 No typesetting found for |- ( ps' <-> A. i e. _om ( suc i e. m -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) with typecode |-
bnj535.3 ⊢ G = f ∪ m ⋃ y ∈ f ⁡ p pred y A R
bnj535.4 No typesetting found for |- ( ta <-> ( ph' /\ ps' /\ m e. _om /\ p e. m ) ) with typecode |-
Assertion bnj535 ⊢ R FrSe A ∧ τ ∧ n = m ∪ m ∧ f Fn m → G Fn n

Proof

Step Hyp Ref Expression
1 bnj535.1 Could not format ( ph' <-> ( f ` (/) ) = _pred ( x , A , R ) ) : No typesetting found for |- ( ph' <-> ( f ` (/) ) = _pred ( x , A , R ) ) with typecode |-
2 bnj535.2 Could not format ( ps' <-> A. i e. _om ( suc i e. m -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) : No typesetting found for |- ( ps' <-> A. i e. _om ( suc i e. m -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) ) with typecode |-
3 bnj535.3 ⊢ G = f ∪ m ⋃ y ∈ f ⁡ p pred y A R
4 bnj535.4 Could not format ( ta <-> ( ph' /\ ps' /\ m e. _om /\ p e. m ) ) : No typesetting found for |- ( ta <-> ( ph' /\ ps' /\ m e. _om /\ p e. m ) ) with typecode |-
5 bnj422 ⊢ R FrSe A ∧ τ ∧ n = m ∪ m ∧ f Fn m ↔ n = m ∪ m ∧ f Fn m ∧ R FrSe A ∧ τ
6 bnj251 ⊢ n = m ∪ m ∧ f Fn m ∧ R FrSe A ∧ τ ↔ n = m ∪ m ∧ f Fn m ∧ R FrSe A ∧ τ
7 5 6 bitri ⊢ R FrSe A ∧ τ ∧ n = m ∪ m ∧ f Fn m ↔ n = m ∪ m ∧ f Fn m ∧ R FrSe A ∧ τ
8 fvex ⊢ f ⁡ p ∈ V
9 1 2 4 bnj518 ⊢ R FrSe A ∧ τ → ∀ y ∈ f ⁡ p pred y A R ∈ V
10 iunexg ⊢ f ⁡ p ∈ V ∧ ∀ y ∈ f ⁡ p pred y A R ∈ V → ⋃ y ∈ f ⁡ p pred y A R ∈ V
11 8 9 10 sylancr ⊢ R FrSe A ∧ τ → ⋃ y ∈ f ⁡ p pred y A R ∈ V
12 vex ⊢ m ∈ V
13 12 bnj519 ⊢ ⋃ y ∈ f ⁡ p pred y A R ∈ V → Fun ⁡ m ⋃ y ∈ f ⁡ p pred y A R
14 11 13 syl ⊢ R FrSe A ∧ τ → Fun ⁡ m ⋃ y ∈ f ⁡ p pred y A R
15 dmsnopg ⊢ ⋃ y ∈ f ⁡ p pred y A R ∈ V → dom ⁡ m ⋃ y ∈ f ⁡ p pred y A R = m
16 11 15 syl ⊢ R FrSe A ∧ τ → dom ⁡ m ⋃ y ∈ f ⁡ p pred y A R = m
17 14 16 bnj1422 ⊢ R FrSe A ∧ τ → m ⋃ y ∈ f ⁡ p pred y A R Fn m
18 disjcsn ⊢ m ∩ m = ∅
19 fnun ⊢ f Fn m ∧ m ⋃ y ∈ f ⁡ p pred y A R Fn m ∧ m ∩ m = ∅ → f ∪ m ⋃ y ∈ f ⁡ p pred y A R Fn m ∪ m
20 18 19 mpan2 ⊢ f Fn m ∧ m ⋃ y ∈ f ⁡ p pred y A R Fn m → f ∪ m ⋃ y ∈ f ⁡ p pred y A R Fn m ∪ m
21 17 20 sylan2 ⊢ f Fn m ∧ R FrSe A ∧ τ → f ∪ m ⋃ y ∈ f ⁡ p pred y A R Fn m ∪ m
22 3 fneq1i ⊢ G Fn m ∪ m ↔ f ∪ m ⋃ y ∈ f ⁡ p pred y A R Fn m ∪ m
23 21 22 sylibr ⊢ f Fn m ∧ R FrSe A ∧ τ → G Fn m ∪ m
24 fneq2 ⊢ n = m ∪ m → G Fn n ↔ G Fn m ∪ m
25 23 24 imbitrrid ⊢ n = m ∪ m → f Fn m ∧ R FrSe A ∧ τ → G Fn n
26 25 imp ⊢ n = m ∪ m ∧ f Fn m ∧ R FrSe A ∧ τ → G Fn n
27 7 26 sylbi ⊢ R FrSe A ∧ τ ∧ n = m ∪ m ∧ f Fn m → G Fn n