Metamath Proof Explorer


Theorem bnj1489

Description: Technical lemma for bnj60 . 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 bnj1489.1 B = d | d A x d pred x A R d
bnj1489.2 Y = x f pred x A R
bnj1489.3 C = f | d B f Fn d x d f x = G Y
bnj1489.4 τ f C dom f = x trCl x A R
bnj1489.5 D = x A | ¬ f τ
bnj1489.6 ψ R FrSe A D
bnj1489.7 χ ψ x D y D ¬ y R x
bnj1489.8 No typesetting found for |- ( ta' <-> [. y / x ]. ta ) with typecode |-
bnj1489.9 No typesetting found for |- H = { f | E. y e. _pred ( x , A , R ) ta' } with typecode |-
bnj1489.10 P = H
bnj1489.11 Z = x P pred x A R
bnj1489.12 Q = P x G Z
Assertion bnj1489 χ Q V

Proof

Step Hyp Ref Expression
1 bnj1489.1 B = d | d A x d pred x A R d
2 bnj1489.2 Y = x f pred x A R
3 bnj1489.3 C = f | d B f Fn d x d f x = G Y
4 bnj1489.4 τ f C dom f = x trCl x A R
5 bnj1489.5 D = x A | ¬ f τ
6 bnj1489.6 ψ R FrSe A D
7 bnj1489.7 χ ψ x D y D ¬ y R x
8 bnj1489.8 Could not format ( ta' <-> [. y / x ]. ta ) : No typesetting found for |- ( ta' <-> [. y / x ]. ta ) with typecode |-
9 bnj1489.9 Could not format H = { f | E. y e. _pred ( x , A , R ) ta' } : No typesetting found for |- H = { f | E. y e. _pred ( x , A , R ) ta' } with typecode |-
10 bnj1489.10 P = H
11 bnj1489.11 Z = x P pred x A R
12 bnj1489.12 Q = P x G Z
13 bnj1364 R FrSe A R Se A
14 df-bnj13 R Se A x A pred x A R V
15 13 14 sylib R FrSe A x A pred x A R V
16 6 15 bnj832 ψ x A pred x A R V
17 7 16 bnj835 χ x A pred x A R V
18 5 7 bnj1212 χ x A
19 17 18 bnj1294 χ pred x A R V
20 nfv y ψ
21 nfv y x D
22 nfra1 y y D ¬ y R x
23 20 21 22 nf3an y ψ x D y D ¬ y R x
24 7 23 nfxfr y χ
25 6 simplbi ψ R FrSe A
26 7 25 bnj835 χ R FrSe A
27 26 adantr χ y pred x A R R FrSe A
28 1 2 3 4 5 6 7 8 bnj1388 Could not format ( ch -> A. y e. _pred ( x , A , R ) E. f ta' ) : No typesetting found for |- ( ch -> A. y e. _pred ( x , A , R ) E. f ta' ) with typecode |-
29 28 r19.21bi Could not format ( ( ch /\ y e. _pred ( x , A , R ) ) -> E. f ta' ) : No typesetting found for |- ( ( ch /\ y e. _pred ( x , A , R ) ) -> E. f ta' ) with typecode |-
30 nfv x R FrSe A
31 nfsbc1v x [˙y / x]˙ τ
32 8 31 nfxfr Could not format F/ x ta' : No typesetting found for |- F/ x ta' with typecode |-
33 32 nfex Could not format F/ x E. f ta' : No typesetting found for |- F/ x E. f ta' with typecode |-
34 30 33 nfan Could not format F/ x ( R _FrSe A /\ E. f ta' ) : No typesetting found for |- F/ x ( R _FrSe A /\ E. f ta' ) with typecode |-
35 32 nfeuw Could not format F/ x E! f ta' : No typesetting found for |- F/ x E! f ta' with typecode |-
36 34 35 nfim Could not format F/ x ( ( R _FrSe A /\ E. f ta' ) -> E! f ta' ) : No typesetting found for |- F/ x ( ( R _FrSe A /\ E. f ta' ) -> E! f ta' ) with typecode |-
37 sneq x = y x = y
38 bnj1318 x = y trCl x A R = trCl y A R
39 37 38 uneq12d x = y x trCl x A R = y trCl y A R
40 39 eqeq2d x = y dom f = x trCl x A R dom f = y trCl y A R
41 40 anbi2d x = y f C dom f = x trCl x A R f C dom f = y trCl y A R
42 1 2 3 4 8 bnj1373 Could not format ( ta' <-> ( f e. C /\ dom f = ( { y } u. _trCl ( y , A , R ) ) ) ) : No typesetting found for |- ( ta' <-> ( f e. C /\ dom f = ( { y } u. _trCl ( y , A , R ) ) ) ) with typecode |-
43 41 42 bitr4di Could not format ( x = y -> ( ( f e. C /\ dom f = ( { x } u. _trCl ( x , A , R ) ) ) <-> ta' ) ) : No typesetting found for |- ( x = y -> ( ( f e. C /\ dom f = ( { x } u. _trCl ( x , A , R ) ) ) <-> ta' ) ) with typecode |-
44 43 exbidv Could not format ( x = y -> ( E. f ( f e. C /\ dom f = ( { x } u. _trCl ( x , A , R ) ) ) <-> E. f ta' ) ) : No typesetting found for |- ( x = y -> ( E. f ( f e. C /\ dom f = ( { x } u. _trCl ( x , A , R ) ) ) <-> E. f ta' ) ) with typecode |-
45 44 anbi2d Could not format ( x = y -> ( ( R _FrSe A /\ E. f ( f e. C /\ dom f = ( { x } u. _trCl ( x , A , R ) ) ) ) <-> ( R _FrSe A /\ E. f ta' ) ) ) : No typesetting found for |- ( x = y -> ( ( R _FrSe A /\ E. f ( f e. C /\ dom f = ( { x } u. _trCl ( x , A , R ) ) ) ) <-> ( R _FrSe A /\ E. f ta' ) ) ) with typecode |-
46 43 eubidv Could not format ( x = y -> ( E! f ( f e. C /\ dom f = ( { x } u. _trCl ( x , A , R ) ) ) <-> E! f ta' ) ) : No typesetting found for |- ( x = y -> ( E! f ( f e. C /\ dom f = ( { x } u. _trCl ( x , A , R ) ) ) <-> E! f ta' ) ) with typecode |-
47 45 46 imbi12d Could not format ( x = y -> ( ( ( R _FrSe A /\ E. f ( f e. C /\ dom f = ( { x } u. _trCl ( x , A , R ) ) ) ) -> E! f ( f e. C /\ dom f = ( { x } u. _trCl ( x , A , R ) ) ) ) <-> ( ( R _FrSe A /\ E. f ta' ) -> E! f ta' ) ) ) : No typesetting found for |- ( x = y -> ( ( ( R _FrSe A /\ E. f ( f e. C /\ dom f = ( { x } u. _trCl ( x , A , R ) ) ) ) -> E! f ( f e. C /\ dom f = ( { x } u. _trCl ( x , A , R ) ) ) ) <-> ( ( R _FrSe A /\ E. f ta' ) -> E! f ta' ) ) ) with typecode |-
48 biid f C dom f = x trCl x A R f C dom f = x trCl x A R
49 1 2 3 48 bnj1321 R FrSe A f f C dom f = x trCl x A R ∃! f f C dom f = x trCl x A R
50 36 47 49 chvarfv Could not format ( ( R _FrSe A /\ E. f ta' ) -> E! f ta' ) : No typesetting found for |- ( ( R _FrSe A /\ E. f ta' ) -> E! f ta' ) with typecode |-
51 27 29 50 syl2anc Could not format ( ( ch /\ y e. _pred ( x , A , R ) ) -> E! f ta' ) : No typesetting found for |- ( ( ch /\ y e. _pred ( x , A , R ) ) -> E! f ta' ) with typecode |-
52 51 ex Could not format ( ch -> ( y e. _pred ( x , A , R ) -> E! f ta' ) ) : No typesetting found for |- ( ch -> ( y e. _pred ( x , A , R ) -> E! f ta' ) ) with typecode |-
53 24 52 ralrimi Could not format ( ch -> A. y e. _pred ( x , A , R ) E! f ta' ) : No typesetting found for |- ( ch -> A. y e. _pred ( x , A , R ) E! f ta' ) with typecode |-
54 9 a1i Could not format ( ch -> H = { f | E. y e. _pred ( x , A , R ) ta' } ) : No typesetting found for |- ( ch -> H = { f | E. y e. _pred ( x , A , R ) ta' } ) with typecode |-
55 biid Could not format ( ( _pred ( x , A , R ) e. _V /\ A. y e. _pred ( x , A , R ) E! f ta' /\ H = { f | E. y e. _pred ( x , A , R ) ta' } ) <-> ( _pred ( x , A , R ) e. _V /\ A. y e. _pred ( x , A , R ) E! f ta' /\ H = { f | E. y e. _pred ( x , A , R ) ta' } ) ) : No typesetting found for |- ( ( _pred ( x , A , R ) e. _V /\ A. y e. _pred ( x , A , R ) E! f ta' /\ H = { f | E. y e. _pred ( x , A , R ) ta' } ) <-> ( _pred ( x , A , R ) e. _V /\ A. y e. _pred ( x , A , R ) E! f ta' /\ H = { f | E. y e. _pred ( x , A , R ) ta' } ) ) with typecode |-
56 55 bnj1366 Could not format ( ( _pred ( x , A , R ) e. _V /\ A. y e. _pred ( x , A , R ) E! f ta' /\ H = { f | E. y e. _pred ( x , A , R ) ta' } ) -> H e. _V ) : No typesetting found for |- ( ( _pred ( x , A , R ) e. _V /\ A. y e. _pred ( x , A , R ) E! f ta' /\ H = { f | E. y e. _pred ( x , A , R ) ta' } ) -> H e. _V ) with typecode |-
57 19 53 54 56 syl3anc χ H V
58 57 uniexd χ H V
59 10 58 eqeltrid χ P V
60 snex x G Z V
61 60 a1i χ x G Z V
62 59 61 bnj1149 χ P x G Z V
63 12 62 eqeltrid χ Q V