Metamath Proof Explorer

Theorem bnj1415

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 bnj1415.1 ⊢ B = d | d ⊆ A ∧ ∀ x ∈ d pred x A R ⊆ d
bnj1415.2 ⊢ Y = x f ↾ pred x A R
bnj1415.3 ⊢ C = f | ∃ d ∈ B f Fn d ∧ ∀ x ∈ d f ⁡ x = G ⁡ Y
bnj1415.4 ⊢ τ ↔ f ∈ C ∧ dom ⁡ f = x ∪ trCl x A R
bnj1415.5 ⊢ D = x ∈ A | ¬ ∃ f τ
bnj1415.6 ⊢ ψ ↔ R FrSe A ∧ D ≠ ∅
bnj1415.7 ⊢ χ ↔ ψ ∧ x ∈ D ∧ ∀ y ∈ D ¬ y R x
bnj1415.8 No typesetting found for |- ( ta' <-> [. y / x ]. ta ) with typecode |-
bnj1415.9 No typesetting found for |- H = { f | E. y e. _pred ( x , A , R ) ta' } with typecode |-
bnj1415.10 ⊢ P = ⋃ H
Assertion bnj1415 ⊢ χ → dom ⁡ P = trCl x A R

Proof

Step Hyp Ref Expression
1 bnj1415.1 ⊢ B = d | d ⊆ A ∧ ∀ x ∈ d pred x A R ⊆ d
2 bnj1415.2 ⊢ Y = x f ↾ pred x A R
3 bnj1415.3 ⊢ C = f | ∃ d ∈ B f Fn d ∧ ∀ x ∈ d f ⁡ x = G ⁡ Y
4 bnj1415.4 ⊢ τ ↔ f ∈ C ∧ dom ⁡ f = x ∪ trCl x A R
5 bnj1415.5 ⊢ D = x ∈ A | ¬ ∃ f τ
6 bnj1415.6 ⊢ ψ ↔ R FrSe A ∧ D ≠ ∅
7 bnj1415.7 ⊢ χ ↔ ψ ∧ x ∈ D ∧ ∀ y ∈ D ¬ y R x
8 bnj1415.8 Could not format ( ta' <-> [. y / x ]. ta ) : No typesetting found for |- ( ta' <-> [. y / x ]. ta ) with typecode |-
9 bnj1415.9 Could not format H = { f | E. y e. _pred ( x , A , R ) ta' } : No typesetting found for |- H = { f | E. y e. _pred ( x , A , R ) ta' } with typecode |-
10 bnj1415.10 ⊢ P = ⋃ H
11 6 simplbi ⊢ ψ → R FrSe A
12 7 11 bnj835 ⊢ χ → R FrSe A
13 5 7 bnj1212 ⊢ χ → x ∈ A
14 eqid ⊢ pred x A R ∪ ⋃ y ∈ pred x A R trCl y A R = pred x A R ∪ ⋃ y ∈ pred x A R trCl y A R
15 14 bnj1414 ⊢ R FrSe A ∧ x ∈ A → trCl x A R = pred x A R ∪ ⋃ y ∈ pred x A R trCl y A R
16 12 13 15 syl2anc ⊢ χ → trCl x A R = pred x A R ∪ ⋃ y ∈ pred x A R trCl y A R
17 iunun ⊢ ⋃ y ∈ pred x A R y ∪ trCl y A R = ⋃ y ∈ pred x A R y ∪ ⋃ y ∈ pred x A R trCl y A R
18 iunid ⊢ ⋃ y ∈ pred x A R y = pred x A R
19 18 uneq1i ⊢ ⋃ y ∈ pred x A R y ∪ ⋃ y ∈ pred x A R trCl y A R = pred x A R ∪ ⋃ y ∈ pred x A R trCl y A R
20 17 19 eqtri ⊢ ⋃ y ∈ pred x A R y ∪ trCl y A R = pred x A R ∪ ⋃ y ∈ pred x A R trCl y A R
21 biid ⊢ χ ∧ z ∈ ⋃ y ∈ pred x A R y ∪ trCl y A R ↔ χ ∧ z ∈ ⋃ y ∈ pred x A R y ∪ trCl y A R
22 biid ⊢ χ ∧ z ∈ ⋃ y ∈ pred x A R y ∪ trCl y A R ∧ y ∈ pred x A R ∧ z ∈ y ∪ trCl y A R ↔ χ ∧ z ∈ ⋃ y ∈ pred x A R y ∪ trCl y A R ∧ y ∈ pred x A R ∧ z ∈ y ∪ trCl y A R
23 1 2 3 4 5 6 7 8 9 10 21 22 bnj1398 ⊢ χ → ⋃ y ∈ pred x A R y ∪ trCl y A R = dom ⁡ P
24 20 23 eqtr3id ⊢ χ → pred x A R ∪ ⋃ y ∈ pred x A R trCl y A R = dom ⁡ P
25 16 24 eqtr2d ⊢ χ → dom ⁡ P = trCl x A R