Metamath Proof Explorer


Theorem bnj1501

Description: Technical lemma for bnj1500 . 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 bnj1501.1 B = d | d A x d pred x A R d
bnj1501.2 Y = x f pred x A R
bnj1501.3 C = f | d B f Fn d x d f x = G Y
bnj1501.4 F = C
bnj1501.5 φ R FrSe A x A
bnj1501.6 ψ φ f C x dom f
bnj1501.7 χ ψ d B dom f = d
Assertion bnj1501 R FrSe A x A F x = G x F pred x A R

Proof

Step Hyp Ref Expression
1 bnj1501.1 B = d | d A x d pred x A R d
2 bnj1501.2 Y = x f pred x A R
3 bnj1501.3 C = f | d B f Fn d x d f x = G Y
4 bnj1501.4 F = C
5 bnj1501.5 φ R FrSe A x A
6 bnj1501.6 ψ φ f C x dom f
7 bnj1501.7 χ ψ d B dom f = d
8 5 simprbi φ x A
9 1 2 3 4 bnj60 R FrSe A F Fn A
10 fndm F Fn A dom F = A
11 9 10 syl R FrSe A dom F = A
12 5 11 bnj832 φ dom F = A
13 8 12 eleqtrrd φ x dom F
14 4 dmeqi dom F = dom C
15 3 bnj1317 w C f w C
16 15 bnj1400 dom C = f C dom f
17 14 16 eqtri dom F = f C dom f
18 13 17 eleqtrdi φ x f C dom f
19 18 bnj1405 φ f C x dom f
20 19 6 bnj1209 φ f ψ
21 3 bnj1436 f C d B f Fn d x d f x = G Y
22 21 bnj1299 f C d B f Fn d
23 fndm f Fn d dom f = d
24 22 23 bnj31 f C d B dom f = d
25 6 24 bnj836 ψ d B dom f = d
26 1 2 3 4 5 6 bnj1518 ψ d ψ
27 25 7 26 bnj1521 ψ d χ
28 9 bnj930 R FrSe A Fun F
29 5 28 bnj832 φ Fun F
30 6 29 bnj835 ψ Fun F
31 elssuni f C f C
32 31 4 sseqtrrdi f C f F
33 6 32 bnj836 ψ f F
34 6 simp3bi ψ x dom f
35 30 33 34 bnj1502 ψ F x = f x
36 1 2 3 bnj1514 f C x dom f f x = G Y
37 6 36 bnj836 ψ x dom f f x = G Y
38 37 34 bnj1294 ψ f x = G Y
39 35 38 eqtrd ψ F x = G Y
40 7 39 bnj835 χ F x = G Y
41 7 30 bnj835 χ Fun F
42 7 33 bnj835 χ f F
43 1 bnj1517 d B x d pred x A R d
44 7 43 bnj836 χ x d pred x A R d
45 7 34 bnj835 χ x dom f
46 7 simp3bi χ dom f = d
47 45 46 eleqtrd χ x d
48 44 47 bnj1294 χ pred x A R d
49 48 46 sseqtrrd χ pred x A R dom f
50 41 42 49 bnj1503 χ F pred x A R = f pred x A R
51 50 opeq2d χ x F pred x A R = x f pred x A R
52 51 2 syl6eqr χ x F pred x A R = Y
53 52 fveq2d χ G x F pred x A R = G Y
54 40 53 eqtr4d χ F x = G x F pred x A R
55 27 54 bnj593 ψ d F x = G x F pred x A R
56 1 2 3 4 bnj1519 F x = G x F pred x A R d F x = G x F pred x A R
57 55 56 bnj1397 ψ F x = G x F pred x A R
58 20 57 bnj593 φ f F x = G x F pred x A R
59 1 2 3 4 bnj1520 F x = G x F pred x A R f F x = G x F pred x A R
60 58 59 bnj1397 φ F x = G x F pred x A R
61 5 60 bnj1459 R FrSe A x A F x = G x F pred x A R