Metamath Proof Explorer

Theorem bnj1312

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

Proof

Step Hyp Ref Expression
1 bnj1312.1 ⊢ B = d | d ⊆ A ∧ ∀ x ∈ d pred x A R ⊆ d
2 bnj1312.2 ⊢ Y = x f ↾ pred x A R
3 bnj1312.3 ⊢ C = f | ∃ d ∈ B f Fn d ∧ ∀ x ∈ d f ⁡ x = G ⁡ Y
4 bnj1312.4 ⊢ τ ↔ f ∈ C ∧ dom ⁡ f = x ∪ trCl x A R
5 bnj1312.5 ⊢ D = x ∈ A | ¬ ∃ f τ
6 bnj1312.6 ⊢ ψ ↔ R FrSe A ∧ D ≠ ∅
7 bnj1312.7 ⊢ χ ↔ ψ ∧ x ∈ D ∧ ∀ y ∈ D ¬ y R x
8 bnj1312.8 Could not format ( ta' <-> [. y / x ]. ta ) : No typesetting found for |- ( ta' <-> [. y / x ]. ta ) with typecode |-
9 bnj1312.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 bnj1312.10 ⊢ P = ⋃ H
11 bnj1312.11 ⊢ Z = x P ↾ pred x A R
12 bnj1312.12 ⊢ Q = P ∪ x G ⁡ Z
13 bnj1312.13 ⊢ W = z Q ↾ pred z A R
14 bnj1312.14 ⊢ E = x ∪ trCl x A R
15 6 simplbi ⊢ ψ → R FrSe A
16 5 ssrab3 ⊢ D ⊆ A
17 16 a1i ⊢ ψ → D ⊆ A
18 6 simprbi ⊢ ψ → D ≠ ∅
19 5 bnj1230 ⊢ w ∈ D → ∀ x w ∈ D
20 19 bnj1228 ⊢ R FrSe A ∧ D ⊆ A ∧ D ≠ ∅ → ∃ x ∈ D ∀ y ∈ D ¬ y R x
21 15 17 18 20 syl3anc ⊢ ψ → ∃ x ∈ D ∀ y ∈ D ¬ y R x
22 nfv ⊢ Ⅎ x R FrSe A
23 19 nfcii ⊢ Ⅎ _ x D
24 nfcv ⊢ Ⅎ _ x ∅
25 23 24 nfne ⊢ Ⅎ x D ≠ ∅
26 22 25 nfan ⊢ Ⅎ x R FrSe A ∧ D ≠ ∅
27 6 26 nfxfr ⊢ Ⅎ x ψ
28 27 nf5ri ⊢ ψ → ∀ x ψ
29 21 7 28 bnj1521 ⊢ ψ → ∃ x χ
30 7 simp2bi ⊢ χ → x ∈ D
31 5 bnj1538 ⊢ x ∈ D → ¬ ∃ f τ
32 1 2 3 4 5 6 7 8 9 10 11 12 bnj1489 ⊢ χ → Q ∈ V
33 7 15 bnj835 ⊢ χ → R FrSe A
34 1 2 3 4 5 6 7 8 9 10 bnj1384 ⊢ R FrSe A → Fun ⁡ P
35 33 34 syl ⊢ χ → Fun ⁡ P
36 1 2 3 4 5 6 7 8 9 10 bnj1415 ⊢ χ → dom ⁡ P = trCl x A R
37 35 36 bnj1422 ⊢ χ → P Fn trCl x A R
38 1 2 3 4 5 6 7 8 9 10 11 12 36 bnj1416 ⊢ χ → dom ⁡ Q = x ∪ trCl x A R
39 1 2 3 4 5 6 7 8 9 10 11 12 35 38 36 bnj1421 ⊢ χ → Fun ⁡ Q
40 39 38 bnj1422 ⊢ χ → Q Fn x ∪ trCl x A R
41 1 2 3 4 5 6 7 8 9 10 11 12 13 14 37 40 bnj1423 ⊢ χ → ∀ z ∈ E Q ⁡ z = G ⁡ W
42 14 fneq2i ⊢ Q Fn E ↔ Q Fn x ∪ trCl x A R
43 40 42 sylibr ⊢ χ → Q Fn E
44 1 2 3 4 5 6 7 8 9 10 11 12 13 14 bnj1452 ⊢ χ → E ∈ B
45 1 2 3 4 5 6 7 8 9 10 11 12 13 14 32 41 43 44 bnj1463 ⊢ χ → Q ∈ C
46 45 38 jca ⊢ χ → Q ∈ C ∧ dom ⁡ Q = x ∪ trCl x A R
47 1 2 3 4 5 6 7 8 9 10 11 12 46 bnj1491 ⊢ χ ∧ Q ∈ V → ∃ f f ∈ C ∧ dom ⁡ f = x ∪ trCl x A R
48 32 47 mpdan ⊢ χ → ∃ f f ∈ C ∧ dom ⁡ f = x ∪ trCl x A R
49 48 4 bnj1198 ⊢ χ → ∃ f τ
50 31 49 nsyl3 ⊢ χ → ¬ x ∈ D
51 29 30 50 bnj1304 ⊢ ¬ ψ
52 6 51 bnj1541 ⊢ R FrSe A → D = ∅
53 5 52 bnj1476 ⊢ R FrSe A → ∀ x ∈ A ∃ f τ
54 4 exbii ⊢ ∃ f τ ↔ ∃ f f ∈ C ∧ dom ⁡ f = x ∪ trCl x A R
55 df-rex ⊢ ∃ f ∈ C dom ⁡ f = x ∪ trCl x A R ↔ ∃ f f ∈ C ∧ dom ⁡ f = x ∪ trCl x A R
56 54 55 bitr4i ⊢ ∃ f τ ↔ ∃ f ∈ C dom ⁡ f = x ∪ trCl x A R
57 56 ralbii ⊢ ∀ x ∈ A ∃ f τ ↔ ∀ x ∈ A ∃ f ∈ C dom ⁡ f = x ∪ trCl x A R
58 53 57 sylib ⊢ R FrSe A → ∀ x ∈ A ∃ f ∈ C dom ⁡ f = x ∪ trCl x A R