Metamath Proof Explorer

Theorem bnj1286

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

Proof

Step Hyp Ref Expression
1 bnj1286.1 ⊢ B = d | d ⊆ A ∧ ∀ x ∈ d pred x A R ⊆ d
2 bnj1286.2 ⊢ Y = x f ↾ pred x A R
3 bnj1286.3 ⊢ C = f | ∃ d ∈ B f Fn d ∧ ∀ x ∈ d f ⁡ x = G ⁡ Y
4 bnj1286.4 ⊢ D = dom ⁡ g ∩ dom ⁡ h
5 bnj1286.5 ⊢ E = x ∈ D | g ⁡ x ≠ h ⁡ x
6 bnj1286.6 ⊢ φ ↔ R FrSe A ∧ g ∈ C ∧ h ∈ C ∧ g ↾ D ≠ h ↾ D
7 bnj1286.7 ⊢ ψ ↔ φ ∧ x ∈ E ∧ ∀ y ∈ E ¬ y R x
8 1 2 3 4 5 6 7 bnj1256 ⊢ φ → ∃ d ∈ B g Fn d
9 8 bnj1196 ⊢ φ → ∃ d d ∈ B ∧ g Fn d
10 1 bnj1517 ⊢ d ∈ B → ∀ x ∈ d pred x A R ⊆ d
11 10 adantr ⊢ d ∈ B ∧ g Fn d → ∀ x ∈ d pred x A R ⊆ d
12 fndm ⊢ g Fn d → dom ⁡ g = d
13 sseq2 ⊢ dom ⁡ g = d → pred x A R ⊆ dom ⁡ g ↔ pred x A R ⊆ d
14 13 raleqbi1dv ⊢ dom ⁡ g = d → ∀ x ∈ dom ⁡ g pred x A R ⊆ dom ⁡ g ↔ ∀ x ∈ d pred x A R ⊆ d
15 12 14 syl ⊢ g Fn d → ∀ x ∈ dom ⁡ g pred x A R ⊆ dom ⁡ g ↔ ∀ x ∈ d pred x A R ⊆ d
16 15 adantl ⊢ d ∈ B ∧ g Fn d → ∀ x ∈ dom ⁡ g pred x A R ⊆ dom ⁡ g ↔ ∀ x ∈ d pred x A R ⊆ d
17 11 16 mpbird ⊢ d ∈ B ∧ g Fn d → ∀ x ∈ dom ⁡ g pred x A R ⊆ dom ⁡ g
18 9 17 bnj593 ⊢ φ → ∃ d ∀ x ∈ dom ⁡ g pred x A R ⊆ dom ⁡ g
19 18 bnj937 ⊢ φ → ∀ x ∈ dom ⁡ g pred x A R ⊆ dom ⁡ g
20 7 19 bnj835 ⊢ ψ → ∀ x ∈ dom ⁡ g pred x A R ⊆ dom ⁡ g
21 5 ssrab3 ⊢ E ⊆ D
22 4 bnj1292 ⊢ D ⊆ dom ⁡ g
23 21 22 sstri ⊢ E ⊆ dom ⁡ g
24 23 sseli ⊢ x ∈ E → x ∈ dom ⁡ g
25 7 24 bnj836 ⊢ ψ → x ∈ dom ⁡ g
26 20 25 bnj1294 ⊢ ψ → pred x A R ⊆ dom ⁡ g
27 1 2 3 4 5 6 7 bnj1259 ⊢ φ → ∃ d ∈ B h Fn d
28 27 bnj1196 ⊢ φ → ∃ d d ∈ B ∧ h Fn d
29 10 adantr ⊢ d ∈ B ∧ h Fn d → ∀ x ∈ d pred x A R ⊆ d
30 fndm ⊢ h Fn d → dom ⁡ h = d
31 sseq2 ⊢ dom ⁡ h = d → pred x A R ⊆ dom ⁡ h ↔ pred x A R ⊆ d
32 31 raleqbi1dv ⊢ dom ⁡ h = d → ∀ x ∈ dom ⁡ h pred x A R ⊆ dom ⁡ h ↔ ∀ x ∈ d pred x A R ⊆ d
33 30 32 syl ⊢ h Fn d → ∀ x ∈ dom ⁡ h pred x A R ⊆ dom ⁡ h ↔ ∀ x ∈ d pred x A R ⊆ d
34 33 adantl ⊢ d ∈ B ∧ h Fn d → ∀ x ∈ dom ⁡ h pred x A R ⊆ dom ⁡ h ↔ ∀ x ∈ d pred x A R ⊆ d
35 29 34 mpbird ⊢ d ∈ B ∧ h Fn d → ∀ x ∈ dom ⁡ h pred x A R ⊆ dom ⁡ h
36 28 35 bnj593 ⊢ φ → ∃ d ∀ x ∈ dom ⁡ h pred x A R ⊆ dom ⁡ h
37 36 bnj937 ⊢ φ → ∀ x ∈ dom ⁡ h pred x A R ⊆ dom ⁡ h
38 7 37 bnj835 ⊢ ψ → ∀ x ∈ dom ⁡ h pred x A R ⊆ dom ⁡ h
39 4 bnj1293 ⊢ D ⊆ dom ⁡ h
40 21 39 sstri ⊢ E ⊆ dom ⁡ h
41 40 sseli ⊢ x ∈ E → x ∈ dom ⁡ h
42 7 41 bnj836 ⊢ ψ → x ∈ dom ⁡ h
43 38 42 bnj1294 ⊢ ψ → pred x A R ⊆ dom ⁡ h
44 26 43 ssind ⊢ ψ → pred x A R ⊆ dom ⁡ g ∩ dom ⁡ h
45 44 4 sseqtrrdi ⊢ ψ → pred x A R ⊆ D