This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem bnj1373

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 bnj1373.1 ⊢ B = d | d ⊆ A ∧ ∀ x ∈ d pred x A R ⊆ d
bnj1373.2 ⊢ Y = x f ↾ pred x A R
bnj1373.3 ⊢ C = f | ∃ d ∈ B f Fn d ∧ ∀ x ∈ d f ⁡ x = G ⁡ Y
bnj1373.4 ⊢ τ ↔ f ∈ C ∧ dom ⁡ f = x ∪ trCl x A R
bnj1373.5 No typesetting found for |- ( ta' <-> [. y / x ]. ta ) with typecode |-
Assertion bnj1373 Could not format assertion : No typesetting found for |- ( ta' <-> ( f e. C /\ dom f = ( { y } u. _trCl ( y , A , R ) ) ) ) with typecode |-

Proof

Step Hyp Ref Expression
1 bnj1373.1 ⊢ B = d | d ⊆ A ∧ ∀ x ∈ d pred x A R ⊆ d
2 bnj1373.2 ⊢ Y = x f ↾ pred x A R
3 bnj1373.3 ⊢ C = f | ∃ d ∈ B f Fn d ∧ ∀ x ∈ d f ⁡ x = G ⁡ Y
4 bnj1373.4 ⊢ τ ↔ f ∈ C ∧ dom ⁡ f = x ∪ trCl x A R
5 bnj1373.5 Could not format ( ta' <-> [. y / x ]. ta ) : No typesetting found for |- ( ta' <-> [. y / x ]. ta ) with typecode |-
6 1 bnj1309 ⊢ f ∈ B → ∀ x f ∈ B
7 3 6 bnj1307 ⊢ f ∈ C → ∀ x f ∈ C
8 7 bnj1351 ⊢ f ∈ C ∧ dom ⁡ f = y ∪ trCl y A R → ∀ x f ∈ C ∧ dom ⁡ f = y ∪ trCl y A R
9 8 nf5i ⊢ Ⅎ x f ∈ C ∧ dom ⁡ f = y ∪ trCl y A R
10 sneq ⊢ x = y → x = y
11 bnj1318 ⊢ x = y → trCl x A R = trCl y A R
12 10 11 uneq12d ⊢ x = y → x ∪ trCl x A R = y ∪ trCl y A R
13 12 eqeq2d ⊢ x = y → dom ⁡ f = x ∪ trCl x A R ↔ dom ⁡ f = y ∪ trCl y A R
14 13 anbi2d ⊢ x = y → f ∈ C ∧ dom ⁡ f = x ∪ trCl x A R ↔ f ∈ C ∧ dom ⁡ f = y ∪ trCl y A R
15 4 14 bitrid ⊢ x = y → τ ↔ f ∈ C ∧ dom ⁡ f = y ∪ trCl y A R
16 9 15 sbciegf ⊢ y ∈ V → [˙y / x]˙ τ ↔ f ∈ C ∧ dom ⁡ f = y ∪ trCl y A R
17 16 elv ⊢ [˙y / x]˙ τ ↔ f ∈ C ∧ dom ⁡ f = y ∪ trCl y A R
18 5 17 bitri Could not format ( ta' <-> ( f e. C /\ dom f = ( { y } u. _trCl ( y , A , R ) ) ) ) : No typesetting found for |- ( ta' <-> ( f e. C /\ dom f = ( { y } u. _trCl ( y , A , R ) ) ) ) with typecode |-