Metamath Proof Explorer


Theorem bnj1018g

Description: Version of bnj1018 with less disjoint variable conditions, but requiring ax-13 . (Contributed by Gino Giotto, 27-Mar-2024) (New usage is discouraged.)

Ref Expression
Hypotheses bnj1018.1 φ f = pred X A R
bnj1018.2 ψ i ω suc i n f suc i = y f i pred y A R
bnj1018.3 χ n D f Fn n φ ψ
bnj1018.4 θ R FrSe A X A y trCl X A R z pred y A R
bnj1018.5 τ m ω n = suc m p = suc n
bnj1018.7 No typesetting found for |- ( ph' <-> [. p / n ]. ph ) with typecode |-
bnj1018.8 No typesetting found for |- ( ps' <-> [. p / n ]. ps ) with typecode |-
bnj1018.9 No typesetting found for |- ( ch' <-> [. p / n ]. ch ) with typecode |-
bnj1018.10 No typesetting found for |- ( ph" <-> [. G / f ]. ph' ) with typecode |-
bnj1018.11 No typesetting found for |- ( ps" <-> [. G / f ]. ps' ) with typecode |-
bnj1018.12 No typesetting found for |- ( ch" <-> [. G / f ]. ch' ) with typecode |-
bnj1018.13 D = ω
bnj1018.14 B = f | n D f Fn n φ ψ
bnj1018.15 C = y f m pred y A R
bnj1018.16 G = f n C
bnj1018.26 No typesetting found for |- ( ch" <-> ( p e. D /\ G Fn p /\ ph" /\ ps" ) ) with typecode |-
bnj1018.29 No typesetting found for |- ( ( th /\ ch /\ ta /\ et ) -> ch" ) with typecode |-
bnj1018.30 No typesetting found for |- ( ( th /\ ch /\ ta /\ et ) -> ( ch" /\ i e. _om /\ suc i e. p ) ) with typecode |-
Assertion bnj1018g θ χ η p τ G suc i trCl X A R

Proof

Step Hyp Ref Expression
1 bnj1018.1 φ f = pred X A R
2 bnj1018.2 ψ i ω suc i n f suc i = y f i pred y A R
3 bnj1018.3 χ n D f Fn n φ ψ
4 bnj1018.4 θ R FrSe A X A y trCl X A R z pred y A R
5 bnj1018.5 τ m ω n = suc m p = suc n
6 bnj1018.7 Could not format ( ph' <-> [. p / n ]. ph ) : No typesetting found for |- ( ph' <-> [. p / n ]. ph ) with typecode |-
7 bnj1018.8 Could not format ( ps' <-> [. p / n ]. ps ) : No typesetting found for |- ( ps' <-> [. p / n ]. ps ) with typecode |-
8 bnj1018.9 Could not format ( ch' <-> [. p / n ]. ch ) : No typesetting found for |- ( ch' <-> [. p / n ]. ch ) with typecode |-
9 bnj1018.10 Could not format ( ph" <-> [. G / f ]. ph' ) : No typesetting found for |- ( ph" <-> [. G / f ]. ph' ) with typecode |-
10 bnj1018.11 Could not format ( ps" <-> [. G / f ]. ps' ) : No typesetting found for |- ( ps" <-> [. G / f ]. ps' ) with typecode |-
11 bnj1018.12 Could not format ( ch" <-> [. G / f ]. ch' ) : No typesetting found for |- ( ch" <-> [. G / f ]. ch' ) with typecode |-
12 bnj1018.13 D = ω
13 bnj1018.14 B = f | n D f Fn n φ ψ
14 bnj1018.15 C = y f m pred y A R
15 bnj1018.16 G = f n C
16 bnj1018.26 Could not format ( ch" <-> ( p e. D /\ G Fn p /\ ph" /\ ps" ) ) : No typesetting found for |- ( ch" <-> ( p e. D /\ G Fn p /\ ph" /\ ps" ) ) with typecode |-
17 bnj1018.29 Could not format ( ( th /\ ch /\ ta /\ et ) -> ch" ) : No typesetting found for |- ( ( th /\ ch /\ ta /\ et ) -> ch" ) with typecode |-
18 bnj1018.30 Could not format ( ( th /\ ch /\ ta /\ et ) -> ( ch" /\ i e. _om /\ suc i e. p ) ) : No typesetting found for |- ( ( th /\ ch /\ ta /\ et ) -> ( ch" /\ i e. _om /\ suc i e. p ) ) with typecode |-
19 df-bnj17 θ χ η p τ θ χ η p τ
20 bnj258 θ χ τ η θ χ η τ
21 20 17 sylbir Could not format ( ( ( th /\ ch /\ et ) /\ ta ) -> ch" ) : No typesetting found for |- ( ( ( th /\ ch /\ et ) /\ ta ) -> ch" ) with typecode |-
22 21 ex Could not format ( ( th /\ ch /\ et ) -> ( ta -> ch" ) ) : No typesetting found for |- ( ( th /\ ch /\ et ) -> ( ta -> ch" ) ) with typecode |-
23 22 eximdv Could not format ( ( th /\ ch /\ et ) -> ( E. p ta -> E. p ch" ) ) : No typesetting found for |- ( ( th /\ ch /\ et ) -> ( E. p ta -> E. p ch" ) ) with typecode |-
24 3 8 11 13 15 bnj985 Could not format ( G e. B <-> E. p ch" ) : No typesetting found for |- ( G e. B <-> E. p ch" ) with typecode |-
25 23 24 syl6ibr θ χ η p τ G B
26 25 imp θ χ η p τ G B
27 19 26 sylbi θ χ η p τ G B
28 bnj1019 p θ χ τ η θ χ η p τ
29 18 simp3d θ χ τ η suc i p
30 16 bnj1235 Could not format ( ch" -> G Fn p ) : No typesetting found for |- ( ch" -> G Fn p ) with typecode |-
31 fndm G Fn p dom G = p
32 17 30 31 3syl θ χ τ η dom G = p
33 29 32 eleqtrrd θ χ τ η suc i dom G
34 33 exlimiv p θ χ τ η suc i dom G
35 28 34 sylbir θ χ η p τ suc i dom G
36 15 bnj918 G V
37 vex i V
38 37 sucex suc i V
39 1 2 12 13 36 38 bnj1015 G B suc i dom G G suc i trCl X A R
40 27 35 39 syl2anc θ χ η p τ G suc i trCl X A R