Metamath Proof Explorer

Theorem bnj1245

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

Proof

Step Hyp Ref Expression
1 bnj1245.1 ⊢ B = d | d ⊆ A ∧ ∀ x ∈ d pred x A R ⊆ d
2 bnj1245.2 ⊢ Y = x f ↾ pred x A R
3 bnj1245.3 ⊢ C = f | ∃ d ∈ B f Fn d ∧ ∀ x ∈ d f ⁡ x = G ⁡ Y
4 bnj1245.4 ⊢ D = dom ⁡ g ∩ dom ⁡ h
5 bnj1245.5 ⊢ E = x ∈ D | g ⁡ x ≠ h ⁡ x
6 bnj1245.6 ⊢ φ ↔ R FrSe A ∧ g ∈ C ∧ h ∈ C ∧ g ↾ D ≠ h ↾ D
7 bnj1245.7 ⊢ ψ ↔ φ ∧ x ∈ E ∧ ∀ y ∈ E ¬ y R x
8 bnj1245.8 ⊢ Z = x h ↾ pred x A R
9 bnj1245.9 ⊢ K = h | ∃ d ∈ B h Fn d ∧ ∀ x ∈ d h ⁡ x = G ⁡ Z
10 6 bnj1247 ⊢ φ → h ∈ C
11 2 3 8 9 bnj1234 ⊢ C = K
12 10 11 eleqtrdi ⊢ φ → h ∈ K
13 9 eqabri ⊢ h ∈ K ↔ ∃ d ∈ B h Fn d ∧ ∀ x ∈ d h ⁡ x = G ⁡ Z
14 13 bnj1238 ⊢ h ∈ K → ∃ d ∈ B h Fn d
15 14 bnj1196 ⊢ h ∈ K → ∃ d d ∈ B ∧ h Fn d
16 1 eqabri ⊢ d ∈ B ↔ d ⊆ A ∧ ∀ x ∈ d pred x A R ⊆ d
17 16 simplbi ⊢ d ∈ B → d ⊆ A
18 fndm ⊢ h Fn d → dom ⁡ h = d
19 17 18 bnj1241 ⊢ d ∈ B ∧ h Fn d → dom ⁡ h ⊆ A
20 15 19 bnj593 ⊢ h ∈ K → ∃ d dom ⁡ h ⊆ A
21 20 bnj937 ⊢ h ∈ K → dom ⁡ h ⊆ A
22 12 21 syl ⊢ φ → dom ⁡ h ⊆ A