Metamath Proof Explorer

Theorem bnj1493

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 bnj1493.1 ⊢ B = d | d ⊆ A ∧ ∀ x ∈ d pred x A R ⊆ d
bnj1493.2 ⊢ Y = x f ↾ pred x A R
bnj1493.3 ⊢ C = f | ∃ d ∈ B f Fn d ∧ ∀ x ∈ d f ⁡ x = G ⁡ Y
Assertion bnj1493 ⊢ R FrSe A → ∀ x ∈ A ∃ f ∈ C dom ⁡ f = x ∪ trCl x A R

Proof

Step Hyp Ref Expression
1 bnj1493.1 ⊢ B = d | d ⊆ A ∧ ∀ x ∈ d pred x A R ⊆ d
2 bnj1493.2 ⊢ Y = x f ↾ pred x A R
3 bnj1493.3 ⊢ C = f | ∃ d ∈ B f Fn d ∧ ∀ x ∈ d f ⁡ x = G ⁡ Y
4 biid ⊢ f ∈ C ∧ dom ⁡ f = x ∪ trCl x A R ↔ f ∈ C ∧ dom ⁡ f = x ∪ trCl x A R
5 eqid ⊢ x ∈ A | ¬ ∃ f f ∈ C ∧ dom ⁡ f = x ∪ trCl x A R = x ∈ A | ¬ ∃ f f ∈ C ∧ dom ⁡ f = x ∪ trCl x A R
6 biid ⊢ R FrSe A ∧ x ∈ A | ¬ ∃ f f ∈ C ∧ dom ⁡ f = x ∪ trCl x A R ≠ ∅ ↔ R FrSe A ∧ x ∈ A | ¬ ∃ f f ∈ C ∧ dom ⁡ f = x ∪ trCl x A R ≠ ∅
7 biid ⊢ R FrSe A ∧ x ∈ A | ¬ ∃ f f ∈ C ∧ dom ⁡ f = x ∪ trCl x A R ≠ ∅ ∧ x ∈ x ∈ A | ¬ ∃ f f ∈ C ∧ dom ⁡ f = x ∪ trCl x A R ∧ ∀ y ∈ x ∈ A | ¬ ∃ f f ∈ C ∧ dom ⁡ f = x ∪ trCl x A R ¬ y R x ↔ R FrSe A ∧ x ∈ A | ¬ ∃ f f ∈ C ∧ dom ⁡ f = x ∪ trCl x A R ≠ ∅ ∧ x ∈ x ∈ A | ¬ ∃ f f ∈ C ∧ dom ⁡ f = x ∪ trCl x A R ∧ ∀ y ∈ x ∈ A | ¬ ∃ f f ∈ C ∧ dom ⁡ f = x ∪ trCl x A R ¬ y R x
8 biid ⊢ [˙y / x]˙ f ∈ C ∧ dom ⁡ f = x ∪ trCl x A R ↔ [˙y / x]˙ f ∈ C ∧ dom ⁡ f = x ∪ trCl x A R
9 eqid ⊢ f | ∃ y ∈ pred x A R [˙y / x]˙ f ∈ C ∧ dom ⁡ f = x ∪ trCl x A R = f | ∃ y ∈ pred x A R [˙y / x]˙ f ∈ C ∧ dom ⁡ f = x ∪ trCl x A R
10 eqid ⊢ ⋃ f | ∃ y ∈ pred x A R [˙y / x]˙ f ∈ C ∧ dom ⁡ f = x ∪ trCl x A R = ⋃ f | ∃ y ∈ pred x A R [˙y / x]˙ f ∈ C ∧ dom ⁡ f = x ∪ trCl x A R
11 eqid ⊢ x ⋃ f | ∃ y ∈ pred x A R [˙y / x]˙ f ∈ C ∧ dom ⁡ f = x ∪ trCl x A R ↾ pred x A R = x ⋃ f | ∃ y ∈ pred x A R [˙y / x]˙ f ∈ C ∧ dom ⁡ f = x ∪ trCl x A R ↾ pred x A R
12 eqid ⊢ ⋃ f | ∃ y ∈ pred x A R [˙y / x]˙ f ∈ C ∧ dom ⁡ f = x ∪ trCl x A R ∪ x G ⁡ x ⋃ f | ∃ y ∈ pred x A R [˙y / x]˙ f ∈ C ∧ dom ⁡ f = x ∪ trCl x A R ↾ pred x A R = ⋃ f | ∃ y ∈ pred x A R [˙y / x]˙ f ∈ C ∧ dom ⁡ f = x ∪ trCl x A R ∪ x G ⁡ x ⋃ f | ∃ y ∈ pred x A R [˙y / x]˙ f ∈ C ∧ dom ⁡ f = x ∪ trCl x A R ↾ pred x A R
13 eqid ⊢ z ⋃ f | ∃ y ∈ pred x A R [˙y / x]˙ f ∈ C ∧ dom ⁡ f = x ∪ trCl x A R ∪ x G ⁡ x ⋃ f | ∃ y ∈ pred x A R [˙y / x]˙ f ∈ C ∧ dom ⁡ f = x ∪ trCl x A R ↾ pred x A R ↾ pred z A R = z ⋃ f | ∃ y ∈ pred x A R [˙y / x]˙ f ∈ C ∧ dom ⁡ f = x ∪ trCl x A R ∪ x G ⁡ x ⋃ f | ∃ y ∈ pred x A R [˙y / x]˙ f ∈ C ∧ dom ⁡ f = x ∪ trCl x A R ↾ pred x A R ↾ pred z A R
14 eqid ⊢ x ∪ trCl x A R = x ∪ trCl x A R
15 1 2 3 4 5 6 7 8 9 10 11 12 13 14 bnj1312 ⊢ R FrSe A → ∀ x ∈ A ∃ f ∈ C dom ⁡ f = x ∪ trCl x A R