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∈dpredxAR⊆d
bnj1452.2 ⊢Y=xf↾predxAR
bnj1452.3 ⊢C=f|∃d∈BfFnd∧∀x∈df⁡x=G⁡Y
bnj1452.4 ⊢τ↔f∈C∧dom⁡f=x∪trClxAR
bnj1452.5 ⊢D=x∈A|¬∃fτ
bnj1452.6 ⊢ψ↔RFrSeA∧D≠∅
bnj1452.7 ⊢χ↔ψ∧x∈D∧∀y∈D¬yRx
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=xP↾predxAR
bnj1452.12 ⊢Q=P∪xG⁡Z
bnj1452.13 ⊢W=zQ↾predzAR
bnj1452.14 ⊢E=x∪trClxAR
Assertion bnj1452 ⊢χ→E∈B

Proof

Step Hyp Ref Expression
1 bnj1452.1 ⊢B=d|d⊆A∧∀x∈dpredxAR⊆d
2 bnj1452.2 ⊢Y=xf↾predxAR
3 bnj1452.3 ⊢C=f|∃d∈BfFnd∧∀x∈df⁡x=G⁡Y
4 bnj1452.4 ⊢τ↔f∈C∧dom⁡f=x∪trClxAR
5 bnj1452.5 ⊢D=x∈A|¬∃fτ
6 bnj1452.6 ⊢ψ↔RFrSeA∧D≠∅
7 bnj1452.7 ⊢χ↔ψ∧x∈D∧∀y∈D¬yRx
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=xP↾predxAR
12 bnj1452.12 ⊢Q=P∪xG⁡Z
13 bnj1452.13 ⊢W=zQ↾predzAR
14 bnj1452.14 ⊢E=x∪trClxAR
15 5 7 bnj1212 ⊢χ→x∈A
16 15 snssd ⊢χ→x⊆A
17 bnj1147 ⊢trClxAR⊆A
18 17 a1i ⊢χ→trClxAR⊆A
19 16 18 unssd ⊢χ→x∪trClxAR⊆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→predzAR=predxAR
24 22 23 syl ⊢χ∧z∈E∧z∈x→predzAR=predxAR
25 6 simplbi ⊢ψ→RFrSeA
26 7 25 bnj835 ⊢χ→RFrSeA
27 bnj906 ⊢RFrSeA∧x∈A→predxAR⊆trClxAR
28 26 15 27 syl2anc ⊢χ→predxAR⊆trClxAR
29 28 ad2antrr ⊢χ∧z∈E∧z∈x→predxAR⊆trClxAR
30 24 29 eqsstrd ⊢χ∧z∈E∧z∈x→predzAR⊆trClxAR
31 ssun4 ⊢predzAR⊆trClxAR→predzAR⊆x∪trClxAR
32 31 14 sseqtrrdi ⊢predzAR⊆trClxAR→predzAR⊆E
33 30 32 syl ⊢χ∧z∈E∧z∈x→predzAR⊆E
34 26 ad2antrr ⊢χ∧z∈E∧z∈trClxAR→RFrSeA
35 simpr ⊢χ∧z∈E∧z∈trClxAR→z∈trClxAR
36 17 35 bnj1213 ⊢χ∧z∈E∧z∈trClxAR→z∈A
37 bnj906 ⊢RFrSeA∧z∈A→predzAR⊆trClzAR
38 34 36 37 syl2anc ⊢χ∧z∈E∧z∈trClxAR→predzAR⊆trClzAR
39 15 ad2antrr ⊢χ∧z∈E∧z∈trClxAR→x∈A
40 bnj1125 ⊢RFrSeA∧x∈A∧z∈trClxAR→trClzAR⊆trClxAR
41 34 39 35 40 syl3anc ⊢χ∧z∈E∧z∈trClxAR→trClzAR⊆trClxAR
42 38 41 sstrd ⊢χ∧z∈E∧z∈trClxAR→predzAR⊆trClxAR
43 42 32 syl ⊢χ∧z∈E∧z∈trClxAR→predzAR⊆E
44 14 bnj1424 ⊢z∈E→z∈x∨z∈trClxAR
45 44 adantl ⊢χ∧z∈E→z∈x∨z∈trClxAR
46 33 43 45 mpjaodan ⊢χ∧z∈E→predzAR⊆E
47 46 ralrimiva ⊢χ→∀z∈EpredzAR⊆E
48 vsnex ⊢x∈V
49 48 a1i ⊢χ→x∈V
50 bnj893 ⊢RFrSeA∧x∈A→trClxAR∈V
51 26 15 50 syl2anc ⊢χ→trClxAR∈V
52 49 51 bnj1149 ⊢χ→x∪trClxAR∈V
53 14 52 eqeltrid ⊢χ→E∈V
54 1 bnj1454 ⊢E∈V→E∈B↔[˙E/d]˙d⊆A∧∀x∈dpredxAR⊆d
55 53 54 syl ⊢χ→E∈B↔[˙E/d]˙d⊆A∧∀x∈dpredxAR⊆d
56 bnj602 ⊢x=z→predxAR=predzAR
57 56 sseq1d ⊢x=z→predxAR⊆d↔predzAR⊆d
58 57 cbvralvw ⊢∀x∈dpredxAR⊆d↔∀z∈dpredzAR⊆d
59 58 anbi2i ⊢d⊆A∧∀x∈dpredxAR⊆d↔d⊆A∧∀z∈dpredzAR⊆d
60 59 sbcbii ⊢[˙E/d]˙d⊆A∧∀x∈dpredxAR⊆d↔[˙E/d]˙d⊆A∧∀z∈dpredzAR⊆d
61 55 60 bitrdi ⊢χ→E∈B↔[˙E/d]˙d⊆A∧∀z∈dpredzAR⊆d
62 sseq1 ⊢d=E→d⊆A↔E⊆A
63 sseq2 ⊢d=E→predzAR⊆d↔predzAR⊆E
64 63 raleqbi1dv ⊢d=E→∀z∈dpredzAR⊆d↔∀z∈EpredzAR⊆E
65 62 64 anbi12d ⊢d=E→d⊆A∧∀z∈dpredzAR⊆d↔E⊆A∧∀z∈EpredzAR⊆E
66 65 sbcieg ⊢E∈V→[˙E/d]˙d⊆A∧∀z∈dpredzAR⊆d↔E⊆A∧∀z∈EpredzAR⊆E
67 53 66 syl ⊢χ→[˙E/d]˙d⊆A∧∀z∈dpredzAR⊆d↔E⊆A∧∀z∈EpredzAR⊆E
68 61 67 bitrd ⊢χ→E∈B↔E⊆A∧∀z∈EpredzAR⊆E
69 20 47 68 mpbir2and ⊢χ→E∈B