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

Metamath Proof Explorer

Theorem bnj944

Description: Technical lemma for bnj69 . 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 bnj944.1 ⊢ φ ↔ f ⁡ ∅ = pred X A R
bnj944.2 ⊢ ψ ↔ ∀ i ∈ ω suc ⁡ i ∈ n → f ⁡ suc ⁡ i = ⋃ y ∈ f ⁡ i pred y A R
bnj944.3 ⊢ χ ↔ n ∈ D ∧ f Fn n ∧ φ ∧ ψ
bnj944.4 No typesetting found for |- ( ph' <-> [. p / n ]. ph ) with typecode |-
bnj944.7 No typesetting found for |- ( ph" <-> [. G / f ]. ph' ) with typecode |-
bnj944.10 ⊢ D = ω ∖ ∅
bnj944.12 ⊢ C = ⋃ y ∈ f ⁡ m pred y A R
bnj944.13 ⊢ G = f ∪ n C
bnj944.14 ⊢ τ ↔ f Fn n ∧ φ ∧ ψ
bnj944.15 ⊢ σ ↔ n ∈ D ∧ p = suc ⁡ n ∧ m ∈ n
Assertion bnj944 Could not format assertion : No typesetting found for |- ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) ) -> ph" ) with typecode |-

Proof

Step Hyp Ref Expression
1 bnj944.1 ⊢ φ ↔ f ⁡ ∅ = pred X A R
2 bnj944.2 ⊢ ψ ↔ ∀ i ∈ ω suc ⁡ i ∈ n → f ⁡ suc ⁡ i = ⋃ y ∈ f ⁡ i pred y A R
3 bnj944.3 ⊢ χ ↔ n ∈ D ∧ f Fn n ∧ φ ∧ ψ
4 bnj944.4 Could not format ( ph' <-> [. p / n ]. ph ) : No typesetting found for |- ( ph' <-> [. p / n ]. ph ) with typecode |-
5 bnj944.7 Could not format ( ph" <-> [. G / f ]. ph' ) : No typesetting found for |- ( ph" <-> [. G / f ]. ph' ) with typecode |-
6 bnj944.10 ⊢ D = ω ∖ ∅
7 bnj944.12 ⊢ C = ⋃ y ∈ f ⁡ m pred y A R
8 bnj944.13 ⊢ G = f ∪ n C
9 bnj944.14 ⊢ τ ↔ f Fn n ∧ φ ∧ ψ
10 bnj944.15 ⊢ σ ↔ n ∈ D ∧ p = suc ⁡ n ∧ m ∈ n
11 simpl ⊢ R FrSe A ∧ X ∈ A ∧ χ ∧ n = suc ⁡ m ∧ p = suc ⁡ n → R FrSe A ∧ X ∈ A
12 bnj667 ⊢ n ∈ D ∧ f Fn n ∧ φ ∧ ψ → f Fn n ∧ φ ∧ ψ
13 3 12 sylbi ⊢ χ → f Fn n ∧ φ ∧ ψ
14 13 9 sylibr ⊢ χ → τ
15 14 3ad2ant1 ⊢ χ ∧ n = suc ⁡ m ∧ p = suc ⁡ n → τ
16 15 adantl ⊢ R FrSe A ∧ X ∈ A ∧ χ ∧ n = suc ⁡ m ∧ p = suc ⁡ n → τ
17 3 bnj1232 ⊢ χ → n ∈ D
18 vex ⊢ m ∈ V
19 18 bnj216 ⊢ n = suc ⁡ m → m ∈ n
20 id ⊢ p = suc ⁡ n → p = suc ⁡ n
21 17 19 20 3anim123i ⊢ χ ∧ n = suc ⁡ m ∧ p = suc ⁡ n → n ∈ D ∧ m ∈ n ∧ p = suc ⁡ n
22 3ancomb ⊢ n ∈ D ∧ p = suc ⁡ n ∧ m ∈ n ↔ n ∈ D ∧ m ∈ n ∧ p = suc ⁡ n
23 10 22 bitri ⊢ σ ↔ n ∈ D ∧ m ∈ n ∧ p = suc ⁡ n
24 21 23 sylibr ⊢ χ ∧ n = suc ⁡ m ∧ p = suc ⁡ n → σ
25 24 adantl ⊢ R FrSe A ∧ X ∈ A ∧ χ ∧ n = suc ⁡ m ∧ p = suc ⁡ n → σ
26 bnj253 ⊢ R FrSe A ∧ X ∈ A ∧ τ ∧ σ ↔ R FrSe A ∧ X ∈ A ∧ τ ∧ σ
27 11 16 25 26 syl3anbrc ⊢ R FrSe A ∧ X ∈ A ∧ χ ∧ n = suc ⁡ m ∧ p = suc ⁡ n → R FrSe A ∧ X ∈ A ∧ τ ∧ σ
28 6 9 10 1 2 bnj938 ⊢ R FrSe A ∧ X ∈ A ∧ τ ∧ σ → ⋃ y ∈ f ⁡ m pred y A R ∈ V
29 7 28 eqeltrid ⊢ R FrSe A ∧ X ∈ A ∧ τ ∧ σ → C ∈ V
30 27 29 syl ⊢ R FrSe A ∧ X ∈ A ∧ χ ∧ n = suc ⁡ m ∧ p = suc ⁡ n → C ∈ V
31 bnj658 ⊢ n ∈ D ∧ f Fn n ∧ φ ∧ ψ → n ∈ D ∧ f Fn n ∧ φ
32 3 31 sylbi ⊢ χ → n ∈ D ∧ f Fn n ∧ φ
33 32 3ad2ant1 ⊢ χ ∧ n = suc ⁡ m ∧ p = suc ⁡ n → n ∈ D ∧ f Fn n ∧ φ
34 simp3 ⊢ χ ∧ n = suc ⁡ m ∧ p = suc ⁡ n → p = suc ⁡ n
35 bnj291 ⊢ n ∈ D ∧ p = suc ⁡ n ∧ f Fn n ∧ φ ↔ n ∈ D ∧ f Fn n ∧ φ ∧ p = suc ⁡ n
36 33 34 35 sylanbrc ⊢ χ ∧ n = suc ⁡ m ∧ p = suc ⁡ n → n ∈ D ∧ p = suc ⁡ n ∧ f Fn n ∧ φ
37 36 adantl ⊢ R FrSe A ∧ X ∈ A ∧ χ ∧ n = suc ⁡ m ∧ p = suc ⁡ n → n ∈ D ∧ p = suc ⁡ n ∧ f Fn n ∧ φ
38 opeq2 ⊢ C = if C ∈ V C ∅ → n C = n if C ∈ V C ∅
39 38 sneqd ⊢ C = if C ∈ V C ∅ → n C = n if C ∈ V C ∅
40 39 uneq2d ⊢ C = if C ∈ V C ∅ → f ∪ n C = f ∪ n if C ∈ V C ∅
41 8 40 eqtrid ⊢ C = if C ∈ V C ∅ → G = f ∪ n if C ∈ V C ∅
42 41 sbceq1d Could not format ( C = if ( C e. _V , C , (/) ) -> ( [. G / f ]. ph' <-> [. ( f u. { <. n , if ( C e. _V , C , (/) ) >. } ) / f ]. ph' ) ) : No typesetting found for |- ( C = if ( C e. _V , C , (/) ) -> ( [. G / f ]. ph' <-> [. ( f u. { <. n , if ( C e. _V , C , (/) ) >. } ) / f ]. ph' ) ) with typecode |-
43 5 42 bitrid Could not format ( C = if ( C e. _V , C , (/) ) -> ( ph" <-> [. ( f u. { <. n , if ( C e. _V , C , (/) ) >. } ) / f ]. ph' ) ) : No typesetting found for |- ( C = if ( C e. _V , C , (/) ) -> ( ph" <-> [. ( f u. { <. n , if ( C e. _V , C , (/) ) >. } ) / f ]. ph' ) ) with typecode |-
44 43 imbi2d Could not format ( C = if ( C e. _V , C , (/) ) -> ( ( ( n e. D /\ p = suc n /\ f Fn n /\ ph ) -> ph" ) <-> ( ( n e. D /\ p = suc n /\ f Fn n /\ ph ) -> [. ( f u. { <. n , if ( C e. _V , C , (/) ) >. } ) / f ]. ph' ) ) ) : No typesetting found for |- ( C = if ( C e. _V , C , (/) ) -> ( ( ( n e. D /\ p = suc n /\ f Fn n /\ ph ) -> ph" ) <-> ( ( n e. D /\ p = suc n /\ f Fn n /\ ph ) -> [. ( f u. { <. n , if ( C e. _V , C , (/) ) >. } ) / f ]. ph' ) ) ) with typecode |-
45 biid Could not format ( [. ( f u. { <. n , if ( C e. _V , C , (/) ) >. } ) / f ]. ph' <-> [. ( f u. { <. n , if ( C e. _V , C , (/) ) >. } ) / f ]. ph' ) : No typesetting found for |- ( [. ( f u. { <. n , if ( C e. _V , C , (/) ) >. } ) / f ]. ph' <-> [. ( f u. { <. n , if ( C e. _V , C , (/) ) >. } ) / f ]. ph' ) with typecode |-
46 eqid ⊢ f ∪ n if C ∈ V C ∅ = f ∪ n if C ∈ V C ∅
47 0ex ⊢ ∅ ∈ V
48 47 elimel ⊢ if C ∈ V C ∅ ∈ V
49 1 4 45 6 46 48 bnj929 Could not format ( ( n e. D /\ p = suc n /\ f Fn n /\ ph ) -> [. ( f u. { <. n , if ( C e. _V , C , (/) ) >. } ) / f ]. ph' ) : No typesetting found for |- ( ( n e. D /\ p = suc n /\ f Fn n /\ ph ) -> [. ( f u. { <. n , if ( C e. _V , C , (/) ) >. } ) / f ]. ph' ) with typecode |-
50 44 49 dedth Could not format ( C e. _V -> ( ( n e. D /\ p = suc n /\ f Fn n /\ ph ) -> ph" ) ) : No typesetting found for |- ( C e. _V -> ( ( n e. D /\ p = suc n /\ f Fn n /\ ph ) -> ph" ) ) with typecode |-
51 30 37 50 sylc Could not format ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) ) -> ph" ) : No typesetting found for |- ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) ) -> ph" ) with typecode |-