Metamath Proof Explorer


Theorem bnj1523

Description: Technical lemma for bnj1522 . 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 bnj1523.1 B = d | d A x d pred x A R d
bnj1523.2 Y = x f pred x A R
bnj1523.3 C = f | d B f Fn d x d f x = G Y
bnj1523.4 F = C
bnj1523.5 φ R FrSe A H Fn A x A H x = G x H pred x A R
bnj1523.6 ψ φ F H
bnj1523.7 χ ψ x A F x H x
bnj1523.8 D = x A | F x H x
bnj1523.9 θ χ y D z D ¬ z R y
Assertion bnj1523 R FrSe A H Fn A x A H x = G x H pred x A R F = H

Proof

Step Hyp Ref Expression
1 bnj1523.1 B = d | d A x d pred x A R d
2 bnj1523.2 Y = x f pred x A R
3 bnj1523.3 C = f | d B f Fn d x d f x = G Y
4 bnj1523.4 F = C
5 bnj1523.5 φ R FrSe A H Fn A x A H x = G x H pred x A R
6 bnj1523.6 ψ φ F H
7 bnj1523.7 χ ψ x A F x H x
8 bnj1523.8 D = x A | F x H x
9 bnj1523.9 θ χ y D z D ¬ z R y
10 1 2 3 4 bnj60 R FrSe A F Fn A
11 5 10 bnj835 φ F Fn A
12 6 11 bnj832 ψ F Fn A
13 7 12 bnj835 χ F Fn A
14 9 13 bnj835 θ F Fn A
15 5 simp2bi φ H Fn A
16 6 15 bnj832 ψ H Fn A
17 7 16 bnj835 χ H Fn A
18 9 17 bnj835 θ H Fn A
19 bnj213 pred y A R A
20 19 a1i θ pred y A R A
21 9 simp3bi θ z D ¬ z R y
22 21 bnj1211 θ z z D ¬ z R y
23 con2b z D ¬ z R y z R y ¬ z D
24 23 albii z z D ¬ z R y z z R y ¬ z D
25 22 24 sylib θ z z R y ¬ z D
26 bnj1418 z pred y A R z R y
27 26 imim1i z R y ¬ z D z pred y A R ¬ z D
28 27 alimi z z R y ¬ z D z z pred y A R ¬ z D
29 25 28 syl θ z z pred y A R ¬ z D
30 29 bnj1142 θ z pred y A R ¬ z D
31 1 bnj1309 w B x w B
32 3 31 bnj1307 w C x w C
33 32 nfcii _ x C
34 33 nfuni _ x C
35 4 34 nfcxfr _ x F
36 35 nfcrii w F x w F
37 8 36 bnj1534 D = z A | F z H z
38 30 19 37 bnj1533 θ z pred y A R F z = H z
39 14 18 20 38 bnj1536 θ F pred y A R = H pred y A R
40 39 opeq2d θ y F pred y A R = y H pred y A R
41 40 fveq2d θ G y F pred y A R = G y H pred y A R
42 1 2 3 4 bnj1500 R FrSe A x A F x = G x F pred x A R
43 5 42 bnj835 φ x A F x = G x F pred x A R
44 6 43 bnj832 ψ x A F x = G x F pred x A R
45 7 44 bnj835 χ x A F x = G x F pred x A R
46 45 36 bnj1529 χ y A F y = G y F pred y A R
47 9 46 bnj835 θ y A F y = G y F pred y A R
48 8 ssrab3 D A
49 9 simp2bi θ y D
50 48 49 bnj1213 θ y A
51 47 50 bnj1294 θ F y = G y F pred y A R
52 5 simp3bi φ x A H x = G x H pred x A R
53 6 52 bnj832 ψ x A H x = G x H pred x A R
54 7 53 bnj835 χ x A H x = G x H pred x A R
55 ax-5 v H x v H
56 54 55 bnj1529 χ y A H y = G y H pred y A R
57 9 56 bnj835 θ y A H y = G y H pred y A R
58 57 50 bnj1294 θ H y = G y H pred y A R
59 41 51 58 3eqtr4d θ F y = H y
60 8 36 bnj1534 D = y A | F y H y
61 60 bnj1538 y D F y H y
62 9 61 bnj836 θ F y H y
63 62 neneqd θ ¬ F y = H y
64 59 63 pm2.65i ¬ θ
65 64 nex ¬ y θ
66 5 simp1bi φ R FrSe A
67 6 66 bnj832 ψ R FrSe A
68 7 67 bnj835 χ R FrSe A
69 48 a1i χ D A
70 7 simp2bi χ x A
71 7 simp3bi χ F x H x
72 8 rabeq2i x D x A F x H x
73 70 71 72 sylanbrc χ x D
74 73 ne0d χ D
75 bnj69 R FrSe A D A D y D z D ¬ z R y
76 68 69 74 75 syl3anc χ y D z D ¬ z R y
77 76 9 bnj1209 χ y θ
78 65 77 mto ¬ χ
79 78 nex ¬ x χ
80 6 simprbi ψ F H
81 12 16 80 36 bnj1542 ψ x A F x H x
82 1 2 3 4 5 6 bnj1525 ψ x ψ
83 81 7 82 bnj1521 ψ x χ
84 79 83 mto ¬ ψ
85 6 84 bnj1541 φ F = H
86 5 85 sylbir R FrSe A H Fn A x A H x = G x H pred x A R F = H