Metamath Proof Explorer

Theorem bnj1296

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 bnj1296.1 ⊢ B = d | d ⊆ A ∧ ∀ x ∈ d pred x A R ⊆ d
bnj1296.2 ⊢ Y = x f ↾ pred x A R
bnj1296.3 ⊢ C = f | ∃ d ∈ B f Fn d ∧ ∀ x ∈ d f ⁡ x = G ⁡ Y
bnj1296.4 ⊢ D = dom ⁡ g ∩ dom ⁡ h
bnj1296.5 ⊢ E = x ∈ D | g ⁡ x ≠ h ⁡ x
bnj1296.6 ⊢ φ ↔ R FrSe A ∧ g ∈ C ∧ h ∈ C ∧ g ↾ D ≠ h ↾ D
bnj1296.7 ⊢ ψ ↔ φ ∧ x ∈ E ∧ ∀ y ∈ E ¬ y R x
bnj1296.18 ⊢ ψ → g ↾ pred x A R = h ↾ pred x A R
bnj1296.9 ⊢ Z = x g ↾ pred x A R
bnj1296.10 ⊢ K = g | ∃ d ∈ B g Fn d ∧ ∀ x ∈ d g ⁡ x = G ⁡ Z
bnj1296.11 ⊢ W = x h ↾ pred x A R
bnj1296.12 ⊢ L = h | ∃ d ∈ B h Fn d ∧ ∀ x ∈ d h ⁡ x = G ⁡ W
Assertion bnj1296 ⊢ ψ → g ⁡ x = h ⁡ x

Proof

Step Hyp Ref Expression
1 bnj1296.1 ⊢ B = d | d ⊆ A ∧ ∀ x ∈ d pred x A R ⊆ d
2 bnj1296.2 ⊢ Y = x f ↾ pred x A R
3 bnj1296.3 ⊢ C = f | ∃ d ∈ B f Fn d ∧ ∀ x ∈ d f ⁡ x = G ⁡ Y
4 bnj1296.4 ⊢ D = dom ⁡ g ∩ dom ⁡ h
5 bnj1296.5 ⊢ E = x ∈ D | g ⁡ x ≠ h ⁡ x
6 bnj1296.6 ⊢ φ ↔ R FrSe A ∧ g ∈ C ∧ h ∈ C ∧ g ↾ D ≠ h ↾ D
7 bnj1296.7 ⊢ ψ ↔ φ ∧ x ∈ E ∧ ∀ y ∈ E ¬ y R x
8 bnj1296.18 ⊢ ψ → g ↾ pred x A R = h ↾ pred x A R
9 bnj1296.9 ⊢ Z = x g ↾ pred x A R
10 bnj1296.10 ⊢ K = g | ∃ d ∈ B g Fn d ∧ ∀ x ∈ d g ⁡ x = G ⁡ Z
11 bnj1296.11 ⊢ W = x h ↾ pred x A R
12 bnj1296.12 ⊢ L = h | ∃ d ∈ B h Fn d ∧ ∀ x ∈ d h ⁡ x = G ⁡ W
13 8 opeq2d ⊢ ψ → x g ↾ pred x A R = x h ↾ pred x A R
14 13 9 11 3eqtr4g ⊢ ψ → Z = W
15 14 fveq2d ⊢ ψ → G ⁡ Z = G ⁡ W
16 10 bnj1436 ⊢ g ∈ K → ∃ d ∈ B g Fn d ∧ ∀ x ∈ d g ⁡ x = G ⁡ Z
17 fndm ⊢ g Fn d → dom ⁡ g = d
18 17 anim1i ⊢ g Fn d ∧ ∀ x ∈ d g ⁡ x = G ⁡ Z → dom ⁡ g = d ∧ ∀ x ∈ d g ⁡ x = G ⁡ Z
19 16 18 bnj31 ⊢ g ∈ K → ∃ d ∈ B dom ⁡ g = d ∧ ∀ x ∈ d g ⁡ x = G ⁡ Z
20 raleq ⊢ dom ⁡ g = d → ∀ x ∈ dom ⁡ g g ⁡ x = G ⁡ Z ↔ ∀ x ∈ d g ⁡ x = G ⁡ Z
21 20 pm5.32i ⊢ dom ⁡ g = d ∧ ∀ x ∈ dom ⁡ g g ⁡ x = G ⁡ Z ↔ dom ⁡ g = d ∧ ∀ x ∈ d g ⁡ x = G ⁡ Z
22 21 rexbii ⊢ ∃ d ∈ B dom ⁡ g = d ∧ ∀ x ∈ dom ⁡ g g ⁡ x = G ⁡ Z ↔ ∃ d ∈ B dom ⁡ g = d ∧ ∀ x ∈ d g ⁡ x = G ⁡ Z
23 19 22 sylibr ⊢ g ∈ K → ∃ d ∈ B dom ⁡ g = d ∧ ∀ x ∈ dom ⁡ g g ⁡ x = G ⁡ Z
24 simpr ⊢ dom ⁡ g = d ∧ ∀ x ∈ dom ⁡ g g ⁡ x = G ⁡ Z → ∀ x ∈ dom ⁡ g g ⁡ x = G ⁡ Z
25 23 24 bnj31 ⊢ g ∈ K → ∃ d ∈ B ∀ x ∈ dom ⁡ g g ⁡ x = G ⁡ Z
26 25 bnj1265 ⊢ g ∈ K → ∀ x ∈ dom ⁡ g g ⁡ x = G ⁡ Z
27 2 3 9 10 bnj1234 ⊢ C = K
28 26 27 eleq2s ⊢ g ∈ C → ∀ x ∈ dom ⁡ g g ⁡ x = G ⁡ Z
29 6 28 bnj770 ⊢ φ → ∀ x ∈ dom ⁡ g g ⁡ x = G ⁡ Z
30 7 29 bnj835 ⊢ ψ → ∀ x ∈ dom ⁡ g g ⁡ x = G ⁡ Z
31 4 bnj1292 ⊢ D ⊆ dom ⁡ g
32 5 7 bnj1212 ⊢ ψ → x ∈ D
33 31 32 bnj1213 ⊢ ψ → x ∈ dom ⁡ g
34 30 33 bnj1294 ⊢ ψ → g ⁡ x = G ⁡ Z
35 12 bnj1436 ⊢ h ∈ L → ∃ d ∈ B h Fn d ∧ ∀ x ∈ d h ⁡ x = G ⁡ W
36 fndm ⊢ h Fn d → dom ⁡ h = d
37 36 anim1i ⊢ h Fn d ∧ ∀ x ∈ d h ⁡ x = G ⁡ W → dom ⁡ h = d ∧ ∀ x ∈ d h ⁡ x = G ⁡ W
38 35 37 bnj31 ⊢ h ∈ L → ∃ d ∈ B dom ⁡ h = d ∧ ∀ x ∈ d h ⁡ x = G ⁡ W
39 raleq ⊢ dom ⁡ h = d → ∀ x ∈ dom ⁡ h h ⁡ x = G ⁡ W ↔ ∀ x ∈ d h ⁡ x = G ⁡ W
40 39 pm5.32i ⊢ dom ⁡ h = d ∧ ∀ x ∈ dom ⁡ h h ⁡ x = G ⁡ W ↔ dom ⁡ h = d ∧ ∀ x ∈ d h ⁡ x = G ⁡ W
41 40 rexbii ⊢ ∃ d ∈ B dom ⁡ h = d ∧ ∀ x ∈ dom ⁡ h h ⁡ x = G ⁡ W ↔ ∃ d ∈ B dom ⁡ h = d ∧ ∀ x ∈ d h ⁡ x = G ⁡ W
42 38 41 sylibr ⊢ h ∈ L → ∃ d ∈ B dom ⁡ h = d ∧ ∀ x ∈ dom ⁡ h h ⁡ x = G ⁡ W
43 simpr ⊢ dom ⁡ h = d ∧ ∀ x ∈ dom ⁡ h h ⁡ x = G ⁡ W → ∀ x ∈ dom ⁡ h h ⁡ x = G ⁡ W
44 42 43 bnj31 ⊢ h ∈ L → ∃ d ∈ B ∀ x ∈ dom ⁡ h h ⁡ x = G ⁡ W
45 44 bnj1265 ⊢ h ∈ L → ∀ x ∈ dom ⁡ h h ⁡ x = G ⁡ W
46 2 3 11 12 bnj1234 ⊢ C = L
47 45 46 eleq2s ⊢ h ∈ C → ∀ x ∈ dom ⁡ h h ⁡ x = G ⁡ W
48 6 47 bnj771 ⊢ φ → ∀ x ∈ dom ⁡ h h ⁡ x = G ⁡ W
49 7 48 bnj835 ⊢ ψ → ∀ x ∈ dom ⁡ h h ⁡ x = G ⁡ W
50 4 bnj1293 ⊢ D ⊆ dom ⁡ h
51 50 32 bnj1213 ⊢ ψ → x ∈ dom ⁡ h
52 49 51 bnj1294 ⊢ ψ → h ⁡ x = G ⁡ W
53 15 34 52 3eqtr4d ⊢ ψ → g ⁡ x = h ⁡ x