Metamath Proof Explorer


Theorem bnj1253

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 bnj1253.1 B = d | d A x d pred x A R d
bnj1253.2 Y = x f pred x A R
bnj1253.3 C = f | d B f Fn d x d f x = G Y
bnj1253.4 D = dom g dom h
bnj1253.5 E = x D | g x h x
bnj1253.6 φ R FrSe A g C h C g D h D
bnj1253.7 ψ φ x E y E ¬ y R x
Assertion bnj1253 φ E

Proof

Step Hyp Ref Expression
1 bnj1253.1 B = d | d A x d pred x A R d
2 bnj1253.2 Y = x f pred x A R
3 bnj1253.3 C = f | d B f Fn d x d f x = G Y
4 bnj1253.4 D = dom g dom h
5 bnj1253.5 E = x D | g x h x
6 bnj1253.6 φ R FrSe A g C h C g D h D
7 bnj1253.7 ψ φ x E y E ¬ y R x
8 6 bnj1254 φ g D h D
9 1 2 3 4 5 6 7 bnj1256 φ d B g Fn d
10 4 bnj1292 D dom g
11 fndm g Fn d dom g = d
12 10 11 sseqtrid g Fn d D d
13 fnssres g Fn d D d g D Fn D
14 12 13 mpdan g Fn d g D Fn D
15 9 14 bnj31 φ d B g D Fn D
16 15 bnj1265 φ g D Fn D
17 1 2 3 4 5 6 7 bnj1259 φ d B h Fn d
18 4 bnj1293 D dom h
19 fndm h Fn d dom h = d
20 18 19 sseqtrid h Fn d D d
21 fnssres h Fn d D d h D Fn D
22 20 21 mpdan h Fn d h D Fn D
23 17 22 bnj31 φ d B h D Fn D
24 23 bnj1265 φ h D Fn D
25 ssid D D
26 fvreseq g D Fn D h D Fn D D D g D D = h D D x D g D x = h D x
27 25 26 mpan2 g D Fn D h D Fn D g D D = h D D x D g D x = h D x
28 16 24 27 syl2anc φ g D D = h D D x D g D x = h D x
29 residm g D D = g D
30 residm h D D = h D
31 29 30 eqeq12i g D D = h D D g D = h D
32 df-ral x D g D x = h D x x x D g D x = h D x
33 28 31 32 3bitr3g φ g D = h D x x D g D x = h D x
34 fvres x D g D x = g x
35 fvres x D h D x = h x
36 34 35 eqeq12d x D g D x = h D x g x = h x
37 36 pm5.74i x D g D x = h D x x D g x = h x
38 37 albii x x D g D x = h D x x x D g x = h x
39 33 38 bitrdi φ g D = h D x x D g x = h x
40 39 necon3abid φ g D h D ¬ x x D g x = h x
41 df-rex x D g x h x x x D g x h x
42 pm4.61 ¬ x D g x = h x x D ¬ g x = h x
43 df-ne g x h x ¬ g x = h x
44 43 anbi2i x D g x h x x D ¬ g x = h x
45 42 44 bitr4i ¬ x D g x = h x x D g x h x
46 45 exbii x ¬ x D g x = h x x x D g x h x
47 exnal x ¬ x D g x = h x ¬ x x D g x = h x
48 41 46 47 3bitr2ri ¬ x x D g x = h x x D g x h x
49 40 48 bitrdi φ g D h D x D g x h x
50 8 49 mpbid φ x D g x h x
51 5 neeq1i E x D | g x h x
52 rabn0 x D | g x h x x D g x h x
53 51 52 bitri E x D g x h x
54 50 53 sylibr φ E