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

Metamath Proof Explorer

Theorem bnj1421

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

Proof

Step Hyp Ref Expression
1 bnj1421.1 ⊢ B = d | d ⊆ A ∧ ∀ x ∈ d pred x A R ⊆ d
2 bnj1421.2 ⊢ Y = x f ↾ pred x A R
3 bnj1421.3 ⊢ C = f | ∃ d ∈ B f Fn d ∧ ∀ x ∈ d f ⁡ x = G ⁡ Y
4 bnj1421.4 ⊢ τ ↔ f ∈ C ∧ dom ⁡ f = x ∪ trCl x A R
5 bnj1421.5 ⊢ D = x ∈ A | ¬ ∃ f τ
6 bnj1421.6 ⊢ ψ ↔ R FrSe A ∧ D ≠ ∅
7 bnj1421.7 ⊢ χ ↔ ψ ∧ x ∈ D ∧ ∀ y ∈ D ¬ y R x
8 bnj1421.8 Could not format ( ta' <-> [. y / x ]. ta ) : No typesetting found for |- ( ta' <-> [. y / x ]. ta ) with typecode |-
9 bnj1421.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 bnj1421.10 ⊢ P = ⋃ H
11 bnj1421.11 ⊢ Z = x P ↾ pred x A R
12 bnj1421.12 ⊢ Q = P ∪ x G ⁡ Z
13 bnj1421.13 ⊢ χ → Fun ⁡ P
14 bnj1421.14 ⊢ χ → dom ⁡ Q = x ∪ trCl x A R
15 bnj1421.15 ⊢ χ → dom ⁡ P = trCl x A R
16 vex ⊢ x ∈ V
17 fvex ⊢ G ⁡ Z ∈ V
18 16 17 funsn ⊢ Fun ⁡ x G ⁡ Z
19 13 18 jctir ⊢ χ → Fun ⁡ P ∧ Fun ⁡ x G ⁡ Z
20 17 dmsnop ⊢ dom ⁡ x G ⁡ Z = x
21 20 a1i ⊢ χ → dom ⁡ x G ⁡ Z = x
22 15 21 ineq12d ⊢ χ → dom ⁡ P ∩ dom ⁡ x G ⁡ Z = trCl x A R ∩ x
23 6 simplbi ⊢ ψ → R FrSe A
24 7 23 bnj835 ⊢ χ → R FrSe A
25 biid ⊢ R FrSe A ↔ R FrSe A
26 biid ⊢ ¬ x ∈ trCl x A R ↔ ¬ x ∈ trCl x A R
27 biid ⊢ ∀ z ∈ A z R x → [˙z / x]˙ ¬ x ∈ trCl x A R ↔ ∀ z ∈ A z R x → [˙z / x]˙ ¬ x ∈ trCl x A R
28 biid ⊢ R FrSe A ∧ x ∈ A ∧ ∀ z ∈ A z R x → [˙z / x]˙ ¬ x ∈ trCl x A R ↔ R FrSe A ∧ x ∈ A ∧ ∀ z ∈ A z R x → [˙z / x]˙ ¬ x ∈ trCl x A R
29 eqid ⊢ pred x A R ∪ ⋃ z ∈ pred x A R trCl z A R = pred x A R ∪ ⋃ z ∈ pred x A R trCl z A R
30 25 26 27 28 29 bnj1417 ⊢ R FrSe A → ∀ x ∈ A ¬ x ∈ trCl x A R
31 disjsn ⊢ trCl x A R ∩ x = ∅ ↔ ¬ x ∈ trCl x A R
32 31 ralbii ⊢ ∀ x ∈ A trCl x A R ∩ x = ∅ ↔ ∀ x ∈ A ¬ x ∈ trCl x A R
33 30 32 sylibr ⊢ R FrSe A → ∀ x ∈ A trCl x A R ∩ x = ∅
34 24 33 syl ⊢ χ → ∀ x ∈ A trCl x A R ∩ x = ∅
35 5 7 bnj1212 ⊢ χ → x ∈ A
36 34 35 bnj1294 ⊢ χ → trCl x A R ∩ x = ∅
37 22 36 eqtrd ⊢ χ → dom ⁡ P ∩ dom ⁡ x G ⁡ Z = ∅
38 funun ⊢ Fun ⁡ P ∧ Fun ⁡ x G ⁡ Z ∧ dom ⁡ P ∩ dom ⁡ x G ⁡ Z = ∅ → Fun ⁡ P ∪ x G ⁡ Z
39 19 37 38 syl2anc ⊢ χ → Fun ⁡ P ∪ x G ⁡ Z
40 12 funeqi ⊢ Fun ⁡ Q ↔ Fun ⁡ P ∪ x G ⁡ Z
41 39 40 sylibr ⊢ χ → Fun ⁡ Q