Metamath Proof Explorer

Theorem bnj1452

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

Proof

Step Hyp Ref Expression
1 bnj1452.1 ⊢ B = d | d ⊆ A ∧ ∀ x ∈ d pred x A R ⊆ d
2 bnj1452.2 ⊢ Y = x f ↾ pred x A R
3 bnj1452.3 ⊢ C = f | ∃ d ∈ B f Fn d ∧ ∀ x ∈ d f ⁡ x = G ⁡ Y
4 bnj1452.4 ⊢ τ ↔ f ∈ C ∧ dom ⁡ f = x ∪ trCl x A R
5 bnj1452.5 ⊢ D = x ∈ A | ¬ ∃ f τ
6 bnj1452.6 ⊢ ψ ↔ R FrSe A ∧ D ≠ ∅
7 bnj1452.7 ⊢ χ ↔ ψ ∧ x ∈ D ∧ ∀ y ∈ D ¬ y R x
8 bnj1452.8 Could not format ( ta' <-> [. y / x ]. ta ) : No typesetting found for |- ( ta' <-> [. y / x ]. ta ) with typecode |-
9 bnj1452.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 bnj1452.10 ⊢ P = ⋃ H
11 bnj1452.11 ⊢ Z = x P ↾ pred x A R
12 bnj1452.12 ⊢ Q = P ∪ x G ⁡ Z
13 bnj1452.13 ⊢ W = z Q ↾ pred z A R
14 bnj1452.14 ⊢ E = x ∪ trCl x A R
15 5 7 bnj1212 ⊢ χ → x ∈ A
16 15 snssd ⊢ χ → x ⊆ A
17 bnj1147 ⊢ trCl x A R ⊆ A
18 17 a1i ⊢ χ → trCl x A R ⊆ A
19 16 18 unssd ⊢ χ → x ∪ trCl x A R ⊆ A
20 14 19 eqsstrid ⊢ χ → E ⊆ A
21 elsni ⊢ z ∈ x → z = x
22 21 adantl ⊢ χ ∧ z ∈ E ∧ z ∈ x → z = x
23 bnj602 ⊢ z = x → pred z A R = pred x A R
24 22 23 syl ⊢ χ ∧ z ∈ E ∧ z ∈ x → pred z A R = pred x A R
25 6 simplbi ⊢ ψ → R FrSe A
26 7 25 bnj835 ⊢ χ → R FrSe A
27 bnj906 ⊢ R FrSe A ∧ x ∈ A → pred x A R ⊆ trCl x A R
28 26 15 27 syl2anc ⊢ χ → pred x A R ⊆ trCl x A R
29 28 ad2antrr ⊢ χ ∧ z ∈ E ∧ z ∈ x → pred x A R ⊆ trCl x A R
30 24 29 eqsstrd ⊢ χ ∧ z ∈ E ∧ z ∈ x → pred z A R ⊆ trCl x A R
31 ssun4 ⊢ pred z A R ⊆ trCl x A R → pred z A R ⊆ x ∪ trCl x A R
32 31 14 sseqtrrdi ⊢ pred z A R ⊆ trCl x A R → pred z A R ⊆ E
33 30 32 syl ⊢ χ ∧ z ∈ E ∧ z ∈ x → pred z A R ⊆ E
34 26 ad2antrr ⊢ χ ∧ z ∈ E ∧ z ∈ trCl x A R → R FrSe A
35 simpr ⊢ χ ∧ z ∈ E ∧ z ∈ trCl x A R → z ∈ trCl x A R
36 17 35 bnj1213 ⊢ χ ∧ z ∈ E ∧ z ∈ trCl x A R → z ∈ A
37 bnj906 ⊢ R FrSe A ∧ z ∈ A → pred z A R ⊆ trCl z A R
38 34 36 37 syl2anc ⊢ χ ∧ z ∈ E ∧ z ∈ trCl x A R → pred z A R ⊆ trCl z A R
39 15 ad2antrr ⊢ χ ∧ z ∈ E ∧ z ∈ trCl x A R → x ∈ A
40 bnj1125 ⊢ R FrSe A ∧ x ∈ A ∧ z ∈ trCl x A R → trCl z A R ⊆ trCl x A R
41 34 39 35 40 syl3anc ⊢ χ ∧ z ∈ E ∧ z ∈ trCl x A R → trCl z A R ⊆ trCl x A R
42 38 41 sstrd ⊢ χ ∧ z ∈ E ∧ z ∈ trCl x A R → pred z A R ⊆ trCl x A R
43 42 32 syl ⊢ χ ∧ z ∈ E ∧ z ∈ trCl x A R → pred z A R ⊆ E
44 14 bnj1424 ⊢ z ∈ E → z ∈ x ∨ z ∈ trCl x A R
45 44 adantl ⊢ χ ∧ z ∈ E → z ∈ x ∨ z ∈ trCl x A R
46 33 43 45 mpjaodan ⊢ χ ∧ z ∈ E → pred z A R ⊆ E
47 46 ralrimiva ⊢ χ → ∀ z ∈ E pred z A R ⊆ E
48 snex ⊢ x ∈ V
49 48 a1i ⊢ χ → x ∈ V
50 bnj893 ⊢ R FrSe A ∧ x ∈ A → trCl x A R ∈ V
51 26 15 50 syl2anc ⊢ χ → trCl x A R ∈ V
52 49 51 bnj1149 ⊢ χ → x ∪ trCl x A R ∈ V
53 14 52 eqeltrid ⊢ χ → E ∈ V
54 1 bnj1454 ⊢ E ∈ V → E ∈ B ↔ [˙E / d]˙ d ⊆ A ∧ ∀ x ∈ d pred x A R ⊆ d
55 53 54 syl ⊢ χ → E ∈ B ↔ [˙E / d]˙ d ⊆ A ∧ ∀ x ∈ d pred x A R ⊆ d
56 bnj602 ⊢ x = z → pred x A R = pred z A R
57 56 sseq1d ⊢ x = z → pred x A R ⊆ d ↔ pred z A R ⊆ d
58 57 cbvralvw ⊢ ∀ x ∈ d pred x A R ⊆ d ↔ ∀ z ∈ d pred z A R ⊆ d
59 58 anbi2i ⊢ d ⊆ A ∧ ∀ x ∈ d pred x A R ⊆ d ↔ d ⊆ A ∧ ∀ z ∈ d pred z A R ⊆ d
60 59 sbcbii ⊢ [˙E / d]˙ d ⊆ A ∧ ∀ x ∈ d pred x A R ⊆ d ↔ [˙E / d]˙ d ⊆ A ∧ ∀ z ∈ d pred z A R ⊆ d
61 55 60 bitrdi ⊢ χ → E ∈ B ↔ [˙E / d]˙ d ⊆ A ∧ ∀ z ∈ d pred z A R ⊆ d
62 sseq1 ⊢ d = E → d ⊆ A ↔ E ⊆ A
63 sseq2 ⊢ d = E → pred z A R ⊆ d ↔ pred z A R ⊆ E
64 63 raleqbi1dv ⊢ d = E → ∀ z ∈ d pred z A R ⊆ d ↔ ∀ z ∈ E pred z A R ⊆ E
65 62 64 anbi12d ⊢ d = E → d ⊆ A ∧ ∀ z ∈ d pred z A R ⊆ d ↔ E ⊆ A ∧ ∀ z ∈ E pred z A R ⊆ E
66 65 sbcieg ⊢ E ∈ V → [˙E / d]˙ d ⊆ A ∧ ∀ z ∈ d pred z A R ⊆ d ↔ E ⊆ A ∧ ∀ z ∈ E pred z A R ⊆ E
67 53 66 syl ⊢ χ → [˙E / d]˙ d ⊆ A ∧ ∀ z ∈ d pred z A R ⊆ d ↔ E ⊆ A ∧ ∀ z ∈ E pred z A R ⊆ E
68 61 67 bitrd ⊢ χ → E ∈ B ↔ E ⊆ A ∧ ∀ z ∈ E pred z A R ⊆ E
69 20 47 68 mpbir2and ⊢ χ → E ∈ B